let A be set ; :: thesis: for B being non empty set
for f being Function of A,B st f is bijective holds
card A = card B
let B be non empty set ; :: thesis: for f being Function of A,B st f is bijective holds
card A = card B
let f be Function of A,B; :: thesis: ( f is bijective implies card A = card B )
assume A1: f is bijective ; :: thesis: card A = card B
then A2: ( f is one-to-one & f is onto ) by FUNCT_2:def 4;
A3: A = dom f by FUNCT_2:def 1;
B c= rng f by FUNCT_2:def 3, A2;
then A4: card B c= card A by A3, CARD_1:28;
rng f c= B by RELAT_1:def 19;
then card A c= card B by A3, CARD_1:26, A2;
hence card A = card B by A4, XBOOLE_0:def 10; :: thesis: verum