let X be set ; :: thesis: for x being object holds
( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
let x be object ; :: thesis: ( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
deffunc H₂( 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 = H₂(y) ) ) from FUNCT_1:sch 3();
thus X,[:X,{x}:] are_equipotent :: thesis: card X = card [:X,{x}:]

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = [:X,{x}:] )
thus f is one-to-one :: thesis: ( dom f = X & rng f = [:X,{x}:] )

proof

let y, z be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y in dom f or not z in dom f or not f . y = f . z or y = z )
assume that
A2: ( y in dom f & z in dom f ) and
A3: f . y = f . z ; :: thesis: y = z
A4: ( [y,x] `1 = y & [z,x] `1 = z ) ;
( f . y = [y,x] & f . z = [z,x] ) by A1, A2;
hence y = z by A3, A4; :: thesis: verum

end;

thus dom f = X by A1; :: thesis: rng f = [:X,{x}:]
thus rng f c= [:X,{x}:] :: according to XBOOLE_0:def 10 :: thesis: [:X,{x}:] c= rng f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [:X,{x}:] )
A5: x in {x} by TARSKI:def 1;
assume y in rng f ; :: thesis: y in [:X,{x}:]
then consider z being object such that
A6: z in dom f and
A7: y = f . z by FUNCT_1:def 3;
y = [z,x] by A1, A6, A7;
hence y in [:X,{x}:] by A1, A6, A5, ZFMISC_1:87; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [:X,{x}:] or y in rng f )
assume y in [:X,{x}:] ; :: thesis: 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; :: thesis: verum

end;

hence card X = card [:X,{x}:] by Th4; :: thesis: verum