let f be Function; :: thesis: card f = card (dom f)
dom f,f are_equipotent

proof

deffunc H₂( set ) -> set = [$1,(f . $1)];
consider g being Function such that
A1: dom g = dom f and
A2: for x being set st x in dom f holds
g . x = H₂(x) from FUNCT_1:sch 3();
take g ; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & proj1 g = dom f & proj2 g = f )
thus g is one-to-one :: thesis: ( proj1 g = dom f & proj2 g = f )

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 g or not b₁ in proj1 g or not g . x = g . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume that
A3: x in dom g and
A4: y in dom g ; :: thesis: ( not g . x = g . y or x = y )
assume g . x = g . y ; :: thesis: x = y
then [x,(f . x)] = g . y by A1, A2, A3
.= [y,(f . y)] by A1, A2, A4 ;
hence x = y by ZFMISC_1:27; :: thesis: verum

end;

thus dom g = dom f by A1; :: thesis: proj2 g = f
thus rng g c= f :: according to XBOOLE_0:def 10 :: thesis: f c= proj2 g

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in rng g or i in f )
assume i in rng g ; :: thesis: i in f
then consider x being set such that
A5: x in dom g and
A6: g . x = i by FUNCT_1:def 3;
g . x = [x,(f . x)] by A1, A2, A5;
hence i in f by A1, A5, A6, FUNCT_1:1; :: thesis: verum

end;

let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in f or [x,b₁] in proj2 g )
let y be set ; :: thesis: ( not [x,y] in f or [x,y] in proj2 g )
assume A7: [x,y] in f ; :: thesis: [x,y] in proj2 g
then A8: x in dom f by FUNCT_1:1;
y = f . x by A7, FUNCT_1:1;
then g . x = [x,y] by A2, A8;
hence [x,y] in proj2 g by A1, A8, FUNCT_1:def 3; :: thesis: verum

end;

hence card f = card (dom f) by Th21; :: thesis: verum