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

proof

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

proof

assume x in rng f ; :: thesis: x in A
then consider y being object such that
A10: y in dom f and
A11: f . y = x by FUNCT_1:def 3;
x = y `1 by A8, A9, A10, A11;
hence x in A by A8, A10, MCART_1:10; :: thesis: verum

end;

set y = the Element of B;
assume A12: x in A ; :: thesis: x in rng f
then A13: [x, the Element of B] in dom f by A8, ZFMISC_1:87;
f . [x, the Element of B] = [x, the Element of B] `1 by A9, A12, ZFMISC_1:87
.= x ;
hence x in rng f by A13, FUNCT_1:def 3; :: thesis: verum

end;

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