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₁( set ) -> set = [:X,{$1}:];
ex f being Function st
( dom f = Y & ( for x being set 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 & ( for x being set st x in Y holds
f . x = H₁(x) ) ) ;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: 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 A2: ( f . x1 = H₁(x1) & f . x2 = H₁(x2) ) by A1;
assume f . x1 = f . x2 ; :: thesis: x1 = x2
then {x1} = {x2} by A2, ZFMISC_1:134;
hence x1 = x2 by ZFMISC_1:6; :: thesis: verum

end;

then A3: f is one-to-one by FUNCT_1:def 8;
for y being set holds
( y in { [:X,{y}:] where y is Element of Y : verum } iff ex x being set st
( x in dom f & y = f . x ) )

proof

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

hereby :: thesis: ( ex x being set 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 set st
( x in dom f & y = f . x )
then consider y' being Element of Y such that
A4: y = [:X,{y'}:] ;
reconsider x = y' as set ;
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 A1, A4; :: thesis: verum

end;

given x being set such that A5: ( x in dom f & y = f . x ) ; :: thesis: y in { [:X,{y}:] where y is Element of Y : verum }
f . x = [:X,{x}:] by A1, A5;
hence y in { [:X,{y}:] where y is Element of Y : verum } by A1, A5; :: thesis: verum

end;

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