Cardinality of two finite sets Definition: Let $A$ be a set, and define $I_n=\{m\mid 1\leq m\leq n\}$ for $n\in\mathbb{N}$. It is said that $A$ is finite if there exist $k\in\mathbb{N}$ such that $A$ and $I_k$ are equinumerous. In this case, the number $k$ is called the cardinality of $A$, written $|A|$.
Then, there's a theorem that says: Let $A$ and $B$ be finite sets. If $f$ is a bijection from $A$ to $B$, then $|A|=|B|$.
My first idea is to construct two functions $f_1,f_2$ that are bijective so that $f_1\circ f_2=f$. It should be something like $A\to I_n$ and $I_n\to B$ for some $n$, but I am unable to define the right functions, as the function $f$ is not explicitly defined. 
Does the other direction hold in the theorem? I.e. if $|A|=|B|$, then there's a bijection between $A$ and $B$?
 A: To save you a lot of headache:
That there is a bijection: $\phi:\mathbb N_k\to A$ means that every $a\in A$ is such that $\phi(j) = n$ for some $j; 1\le j \le k$ [because $\phi$ is onto].  And that no other element $b \in A$ is equal to $\phi(j)$ [because $\phi$ is one to one] and so $b = \phi(l)$ for some other $l$ [because $\phi$ is onto].  And for every $m; 1\le m \le k$ we have $\phi(m) = c$ for some distinct $c \in B$ [because $\phi$ is a function].
If we use the notation that $\phi(j) = a_j \in A$ then:

this means nothing more or less than the elements of $A$ may be written as $\{a_1, a_2, ....., a_k\}$.

Nothing more.  Nothing less.
So $|A| = |B| = k$ means nothing more or less than $A$ can be written as $\{a_1, ... , a_k\}$.  (If we assume $\phi(j) = a_j$ for the bijection $\phi:\mathbb N_k \to A$) And that $B$ can be written as $\{b_1, ...., b_k\}$ (If we assume $\psi(j) = b_j$ is the bijection $\psi:\mathbb N_k \to B$).
We can find a bijection between $f:A\to B$ via $f(a_j) = b_j$ and that's "clearly" a bijection.  (It's onto: for all $b_j\in B$ then we can just map $f(a_j) = b_j$.  It's one to one.  If $a_j \ne a_i$ then $f(a_i) = b_i\ne b_j = f(a_j)$.).
If we want to get technical and work backwards $f: A \to \mathbb N_j \to B$ via $f = \psi\circ \phi^{-1}$.  i.e. $f(a_j) = \psi(\phi^{-1}(a_j)) = \psi(j) = b_j$.  Or $f: a_j \to j \to a_j$.
So from now on out.... all these vague and abstract definitions of cardinality on finite and countable sets... they can be thought of as simply being able to list a count the elements.  And that should make things MUCH easier and a LOT clearer.
... You're welcome.
A: Yes. Order the elements of $A$ and $B$ such that $A = \{a_1, \dots, a_n\}$ and $B = \{b_1, \dots, b_n\}$, where $n \in \mathbb{N}$ such that $|A| = |B| = |I_n|$. Now, you can define your bijection as $f(a_i) = b_i$ for all $i \in I_n$.
A: Two proofs.  
If f is a bijection from A to B, then A,B are
equinumerous and since A equinumerous I$_n$ for
some n in N, B is equinumerous to I$_n$ because
equinumerous is an equivalence relation.  
Assume g:A -> I$_n$ is a bijection for some n.
If f:A -> B is a bijection, then gf$^{-1}$
is a bijection from B to I$_n$.  
To answer your last question, A equinumerous B iff by definition, exists bijection f:A -> B.
A: You don't need to define a bijection to prove the theorem:
Thm: Let $A$ and $B$ be finite sets. If there is a bijection from $A$ to $B$, then $|A|=|B|$
Therefore, to prove the thm stated above, suppose $P$ and show $Q$ since its a conditional.
Suppose, $\exists F\ni \text{$F$ is a bijection from $A$ to $B$ }$. Which means F is injective and surjective, therefore, 
$\forall y \in B (\exists x\in A)\ni F(x)=y$ and $\forall x,y\in A(F(x)=F(y)\implies x=y)$
$$x_i\rightarrow y_m$$
$$x_j\rightarrow y_n$$
$$\vdots\rightarrow \vdots$$
$$x_k\rightarrow y_o$$
Therefore, $|A|$ being nothing but the number of elements in the set $A$ is equal to $|B|$ since there is one-to-one and onto correspondace between the elements of the set. Therefore, $|A|=|B|$.
Yes, the other direction of the conditional holds. Notice, if you have two sets $C$ and $D$ with equal equal elements in both, that is $|C|=|D|$. Then you can define a function that maps every element of $D$ to $C$ or vise-verse. Therefore, we will have a bijection.
