assume A2: [:B,A:] is finite ; :: thesis: contradiction
deffunc H₂( set ) -> set = A `2 ;
consider f being Function such that
A3: dom f = [:B,A:] and
A4: 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
A5: x in dom f and
A6: f . x = y by FUNCT_1:def 5;
y = x `2 by A3, A4, A5, A6;
hence y in A by A3, A5, MCART_1:10; :: thesis: verum

end;

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

end;

then rng f = A by TARSKI:2;
then f .: [:B,A:] = A by A3, RELAT_1:146;
hence contradiction by A2; :: thesis: verum