let X, Y be non empty set ; :: thesis: card { [:X,{y}:] where y is Element of Y : verum } = card Y
set Z = { [:X,{y}:] where y is Element of Y : verum } ;
deffunc H₁( object ) -> set = [:X,{$1}:];
ex f being Function st
( dom f = Y & ( for x being object st x in Y holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
then consider f being Function such that
A1: dom f = Y and
A2: for x being object st x in Y holds
f . x = H₁(x) ;
for y being object holds
( y in { [:X,{y}:] where y is Element of Y : verum } iff ex x being object st
( x in dom f & y = f . x ) )

proof

let y be object ; :: thesis: ( y in { [:X,{y}:] where y is Element of Y : verum } iff ex x being object st
( x in dom f & y = f . x ) )

hereby :: thesis: ( ex x being object st
( x in dom f & y = f . x ) implies y in { [:X,{y}:] where y is Element of Y : verum } )

assume y in { [:X,{y}:] where y is Element of Y : verum } ; :: thesis: ex x being object st
( x in dom f & y = f . x )
then consider y9 being Element of Y such that
A3: y = [:X,{y9}:] ;
reconsider x = y9 as object ;
take x = x; :: thesis: ( x in dom f & y = f . x )
thus x in dom f by A1; :: thesis: y = f . x
thus y = f . x by A2, A3; :: thesis: verum

end;

given x being object such that A4: x in dom f and
A5: y = f . x ; :: thesis: y in { [:X,{y}:] where y is Element of Y : verum }
f . x = [:X,{x}:] by A1, A2, A4;
hence y in { [:X,{y}:] where y is Element of Y : verum } by A1, A4, A5; :: thesis: verum

end;

then A6: rng f = { [:X,{y}:] where y is Element of Y : verum } by FUNCT_1:def 3;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then A7: ( f . x1 = H₁(x1) & f . x2 = H₁(x2) ) by A1, A2;
assume f . x1 = f . x2 ; :: thesis: x1 = x2
then {x1} = {x2} by A7, ZFMISC_1:110;
hence x1 = x2 by ZFMISC_1:3; :: thesis: verum

end;

then f is one-to-one by FUNCT_1:def 4;
then { [:X,{y}:] where y is Element of Y : verum } ,Y are_equipotent by A1, A6, WELLORD2:def 4;
hence card { [:X,{y}:] where y is Element of Y : verum } = card Y by CARD_1:5; :: thesis: verum