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 )

proof

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

proof

assume y in rng f ; :: thesis: y in A
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: verum

end;

set x = the Element of B;
assume A19: y in A ; :: thesis: y in rng f
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: verum

end;

then rng f = A by TARSKI:2;
then A21: f .: [:B,A:] = A by A15, RELAT_1:113;
assume [:B,A:] is finite ; :: thesis: contradiction
hence contradiction by A21; :: thesis: verum