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

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