let A, B be non empty finite set ; :: thesis: ( ex f being Function of A,B st
( f is one-to-one & f is onto ) implies card A = card B )
given f being Function of A,B such that A1: f is one-to-one and
A2: f is onto ; :: thesis: card A = card B
A3: ( A = dom f & rng f c= B ) by FUNCT_2:def 1, RELSET_1:12;
then card A c= card B by A1, CARD_1:26;
then A4: card A <= card B by NAT_1:40;
B c= rng f by A2, FUNCT_2:def 3;
then card B c= card A by A3, CARD_1:28;
then card B <= card A by NAT_1:40;
hence card A = card B by A4, XXREAL_0:1; :: thesis: verum