Description: Define a one-to-one onto function. For equivalent definitions see
dff1o2 , dff1o3 , dff1o4 , and dff1o5 . Compare Definition
6.15(6) of TakeutiZaring p. 27. We use their notation ("1-1" above
the arrow and "onto" below the arrow).

A one-to-one onto function is also called a "bijection" or a "bijective
function", F : A -1-1-onto-> B can be read as " F is a bijection
between A and B ". Bijections are precisely the isomorphisms in
the category SetCat of sets and set functions, see setciso .
Therefore, two sets are called "isomorphic" if there is a bijection
between them. According to isof1oidb , two sets are isomorphic iff
there is an isomorphism Isom regarding the identity relation. In
this case, the two sets are also "equinumerous", see bren .
(Contributed by NM, 1-Aug-1994)