let f be Function; 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
;
WELLORD2:def 4 ( g is one-to-one & dom g = dom f & rng g = f )
thus
g is
one-to-one
( dom g = dom f & rng g = f )
thus
dom g = dom f
by A1;
rng g = f
thus
rng g c= f
XBOOLE_0:def 10 f c= rng g
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in f or [x,y] in rng g )
assume A7:
[x,y] in f
;
[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;
verum
end;
hence
card f = card (dom f)
by Th4; verum