let X, x be set ; :: thesis: ( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
deffunc H₃( set ) -> set = [$1,x];
consider f being Function such that
A1: ( dom f = X & ( for y being set 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 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not y in dom f or not b₁ in dom f or not f . y = f . b₁ or y = b₁ )
let z be set ; :: thesis: ( not y in dom f or not z in dom f or not f . y = f . z or y = z )
assume A2: ( y in dom f & z in dom f & f . y = f . z ) ; :: thesis: y = z
then ( f . y = [y,x] & f . z = [z,x] & [y,x] `1 = y ) by A1, MCART_1:7;
hence y = z by A2, MCART_1:7; :: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [:X,{x}:] )
assume y in rng f ; :: thesis: y in [:X,{x}:]
then consider z being set such that
A3: ( z in dom f & y = f . z ) by FUNCT_1:def 5;
( y = [z,x] & x in {x} ) by A1, A3, TARSKI:def 1;
hence y in [:X,{x}:] by A1, A3, ZFMISC_1:106; :: thesis: verum

end;

let y be set ; :: 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 set such that
A4: ( y1 in X & y2 in {x} & y = [y1,y2] ) by ZFMISC_1:103;
y2 = x by A4, TARSKI:def 1;
then y = f . y1 by A1, A4;
hence y in rng f by A1, A4, FUNCT_1:def 5; :: thesis: verum

end;

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