let X be set ; :: thesis: card { {X,[x,X]} where x is Element of X : x in X } = card X
set uG = X;
set A = { {X,[x,X]} where x is Element of X : x in X } ;
deffunc H₁( set ) -> set = {X,[$1,X]};
consider f being Function such that
B: dom f = X and
D: for x being set st x in X holds
f . x = H₁(x) from FUNCT_1:sch 3();

now :: thesis: for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A1: x1 in dom f and
B1: x2 in dom f and
C1: f . x1 = f . x2 ; :: thesis: x1 = x2
( H₁(x1) = f . x1 & H₁(x2) = f . x2 ) by A1, B1, B, D;
then ( [x1,X] = X or [x1,X] = [x2,X] ) by C1, ZFMISC_1:6;
hence x1 = x2 by Aux2, XTUPLE_0:1; :: thesis: verum

end;

then X: f is one-to-one by FUNCT_1:def 4;
Y: rng f = { {X,[x,X]} where x is Element of X : x in X }

proof

thus rng f c= { {X,[x,X]} where x is Element of X : x in X } :: according to XBOOLE_0:def 10 :: thesis: { {X,[x,X]} where x is Element of X : x in 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,X]} where x is Element of X : x in X } )
assume y in rng f ; :: thesis: y in { {X,[x,X]} where x is Element of X : x in X }
then consider a being set such that
A1: a in dom f and
B1: f . a = y by FUNCT_1:def 3;
y = {X,[a,X]} by A1, B1, B, D;
hence y in { {X,[x,X]} where x is Element of X : x in X } by A1, B; :: thesis: verum

end;

thus { {X,[x,X]} where x is Element of X : x in X } c= rng f :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { {X,[x,X]} where x is Element of X : x in X } or a in rng f )
assume a in { {X,[x,X]} where x is Element of X : x in X } ; :: thesis: a in rng f
then consider x being Element of X such that
A1: a = {X,[x,X]} and
B1: x in X ;
f . x = a by A1, B1, D;
hence a in rng f by B, B1, FUNCT_1:def 3; :: thesis: verum

end;

end;

{ {X,[x,X]} where x is Element of X : x in X } ,X are_equipotent by B, X, Y, WELLORD2:def 4;
hence card { {X,[x,X]} where x is Element of X : x in X } = card X by CARD_1:5; :: thesis: verum