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 by FUNCT_2:def 1;
B c= rng f by A2, FUNCT_2:def 3;
then card B c= card A by A3, CARD_1:28;
then A4: card B <= card A by NAT_1:40;
rng f c= B by RELAT_1:def 19;
then card A c= card B by A1, A3, CARD_1:26;
then card A <= card B by NAT_1:40;
hence card A = card B by A4, XXREAL_0:1; :: thesis: verum