let X, Y be non empty set ; :: thesis:
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 ) )

let y be object ; :: thesis:

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

end;

given x being object such that A4: x in dom f and
A5: y = f . x ; :: thesis:
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:

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

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

end;