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₁( object ) -> set = {X,[$1,X]};
consider f being Function such that
A1: dom f = X and
A2: for x being object st x in X holds
f . x = H₁(x) from FUNCT_1:sch 3();

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

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2
( H₁(x1) = f . x1 & H₁(x2) = f . x2 ) by A3, A4, A1, A2;
then ( [x1,X] = X or [x1,X] = [x2,X] ) by A5, ZFMISC_1:6;
hence x1 = x2 by Th2, XTUPLE_0:1; :: thesis: verum

end;

then A6: f is one-to-one ;
A7: 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 object ; :: 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 object such that
A8: a in dom f and
A9: f . a = y by FUNCT_1:def 3;
y = {X,[a,X]} by A8, A9, A1, A2;
hence y in { {X,[x,X]} where x is Element of X : x in X } by A8, A1; :: 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 object ; :: 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
A10: a = {X,[x,X]} and
A11: x in X ;
f . x = a by A10, A11, A2;
hence a in rng f by A1, A11, FUNCT_1:def 3; :: thesis: verum

end;

end;

{ {X,[x,X]} where x is Element of X : x in X } ,X are_equipotent by A1, A6, A7, 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