let f be Function; :: thesis: card f = card (dom f)
dom f,f are_equipotent
proof
deffunc H2( object ) -> object = [$1,(f . $1)];
consider g being Function such that
A1: dom g = dom f and
A2: for x being object st x in dom f holds
g . x = H2(x) from FUNCT_1:sch 3();
 take g ; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & dom g = dom f & rng g = f )
thus g is one-to-one :: thesis: ( dom g = dom f & rng g = f )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom g or not y in dom 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 XTUPLE_0:1; :: thesis: verum
end;
thus dom g = dom f by A1; :: thesis: rng g = f
thus rng g c= f :: according to XBOOLE_0:def 10 :: thesis: f c= rng g
proof
let i be object ; :: 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 object 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, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in f or [x,y] in rng g )
assume A7: [x,y] in f ; :: thesis: [x,y] in rng 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, A7, FUNCT_1:1;
hence [x,y] in rng g by A1, A8, FUNCT_1:def 3; :: thesis: verum
end;
hence card f = card (dom f) by Th4; :: thesis: verum