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 f is bijective ; :: thesis: card A = card B
then A1: ( f is one-to-one & f is onto ) ;
A2: A = dom f by FUNCT_2:def 1;
B c= rng f by A1;
then A3: card B c= card A by A2, CARD_1:12;
card A c= card B by A2, A1, CARD_1:10;
hence card A = card B by A3; :: thesis: verum