let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y st f is bijective holds
card X = card Y
let Y be non empty set ; :: thesis: for f being Function of X,Y st f is bijective holds
card X = card Y
let f be Function of X,Y; :: thesis: ( f is bijective implies card X = card Y )
assume A1: f is bijective ; :: thesis: card X = card Y
then A2: rng f = Y by FUNCT_2:def 3;
dom f = X by FUNCT_2:def 1;
then A3: card X c= card Y by A1, A2, CARD_1:26;
A4: dom f = rng (f " ) by A1, FUNCT_1:55;
rng f = dom (f " ) by A1, FUNCT_1:55;
then card Y c= card X by A1, A2, A4, CARD_1:26;
hence card X = card Y by A3, XBOOLE_0:def 10; :: thesis: verum