deffunc H₂( object ) -> object = A `2 ;
consider f being Function such that
A15: dom f = [:B,A:] and
A16: for x being object st x in [:B,A:] holds
f . x = H₂(x) from FUNCT_1:sch 3();
for y being object holds
( y in rng f iff y in A )

let y be object ; :: thesis:
thus ( y in rng f implies y in A ) :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A17: x in dom f and
A18: f . x = y by FUNCT_1:def 3;
y = x `2 by A15, A16, A17, A18;
hence y in A by A15, A17, MCART_1:10; :: thesis:

end;

set x = the Element of B;
assume A19: y in A ; :: thesis:
then A20: [ the Element of B,y] in dom f by A15, ZFMISC_1:87;
[ the Element of B,y] `2 = y ;
then f . [ the Element of B,y] = y by A16, A19, ZFMISC_1:87;
hence y in rng f by A20, FUNCT_1:def 3; :: thesis:

end;