let X, x be set ; :: thesis: ( X,{x} are_equipotent iff ex x being set st X = {x} )
thus ( X,{x} are_equipotent implies ex x being set st X = {x} ) :: thesis: ( ex x being set st X = {x} implies X,{x} are_equipotent )

proof

assume X,{x} are_equipotent ; :: thesis: ex x being set st X = {x}
then consider f being Function such that
f is one-to-one and
A1: dom f = {x} and
A2: rng f = X by WELLORD2:def 4;
rng f = {(f . x)} by A1, FUNCT_1:14;
hence ex x being set st X = {x} by A2; :: thesis: verum

end;

given y being set such that A3: X = {y} ; :: thesis: X,{x} are_equipotent
take f = X --> x; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = {x} )
A4: dom f = X by FUNCOP_1:19;
thus f is one-to-one :: thesis: ( dom f = X & rng f = {x} )

proof

let a be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not a in dom f or not b₁ in dom f or not f . a = f . b₁ or a = b₁ )
let b be set ; :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A5: a in dom f and
A6: b in dom f and
f . a = f . b ; :: thesis: a = b
a = y by A3, A4, A5, TARSKI:def 1;
hence a = b by A3, A4, A6, TARSKI:def 1; :: thesis: verum

end;

thus dom f = X by FUNCOP_1:19; :: thesis: rng f = {x}
thus rng f c= {x} by FUNCOP_1:19; :: according to XBOOLE_0:def 10 :: thesis: {x} c= rng f
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} or a in rng f )
assume a in {x} ; :: thesis: a in rng f
then A7: a = x by TARSKI:def 1;
A8: y in {y} by TARSKI:def 1;
then f . y = x by A3, FUNCOP_1:13;
hence a in rng f by A3, A4, A7, A8, FUNCT_1:def 5; :: thesis: verum