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

proof

let y be set ; :: 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 set such that
A16: x in dom f and
A17: f . x = y by FUNCT_1:def 5;
y = x `2 by A14, A15, A16, A17;
hence y in A by A14, A16, MCART_1:10; :: thesis: verum

end;

consider x being Element of B;
assume y in A ; :: thesis: y in rng f
then A18: [x,y] in dom f by A14, ZFMISC_1:106;
[x,y] `2 = y by MCART_1:7;
then f . [x,y] = y by A14, A15, A18;
hence y in rng f by A18, FUNCT_1:def 5; :: thesis: verum

end;

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