let X be set ; for x being object holds
( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
let x be object ; ( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
deffunc H2( object ) -> object = [$1,x];
consider f being Function such that
A1:
( dom f = X & ( for y being object st y in X holds
f . y = H2(y) ) )
from FUNCT_1:sch 3();
thus
X,[:X,{x}:] are_equipotent
card X = card [:X,{x}:]proof
take
f
;
WELLORD2:def 4 ( f is one-to-one & dom f = X & rng f = [:X,{x}:] )
thus
f is
one-to-one
( dom f = X & rng f = [:X,{x}:] )
thus
dom f = X
by A1;
rng f = [:X,{x}:]
thus
rng f c= [:X,{x}:]
XBOOLE_0:def 10 [:X,{x}:] c= rng f
let y be
object ;
TARSKI:def 3 ( not y in [:X,{x}:] or y in rng f )
assume
y in [:X,{x}:]
;
y in rng f
then consider y1,
y2 being
object such that A8:
y1 in X
and A9:
y2 in {x}
and A10:
y = [y1,y2]
by ZFMISC_1:84;
y2 = x
by A9, TARSKI:def 1;
then
y = f . y1
by A1, A8, A10;
hence
y in rng f
by A1, A8, FUNCT_1:def 3;
verum
end;
hence
card X = card [:X,{x}:]
by Th4; verum