let X be set ; :: thesis:
deffunc H₁( object ) -> set = {$1};
consider f being Function such that
A1: ( dom f = X & ( for x being object st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
A2: rng f c= bool X

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def 3;
A5: {y} c= X by A1, A3, TARSKI:def 1;
f . y = {y} by A1, A3;
hence x in bool X by A4, A5; :: thesis:

end;

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A7: ( x in dom f & y in dom f ) and
A8: f . x = f . y ; :: thesis:
( f . x = {x} & f . y = {y} ) by A1, A7;
hence x = y by A8, ZFMISC_1:3; :: thesis:

end;