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

proof

let x be set ; :: 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 set 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 x in A ; :: thesis: x in rng f
then A12: [x, the Element of B] in dom f by A8, ZFMISC_1:87;
then f . [x, the Element of B] = [x, the Element of B] `1 by A8, A9
.= x by MCART_1:7 ;
hence x in rng f by A12, FUNCT_1:def 3; :: thesis: verum

end;

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