let F be Function; :: thesis: ( not dom F is finite & rng F is finite implies ex x being set st
( x in rng F & not F " {x} is finite ) )
assume A1: ( not dom F is finite & rng F is finite ) ; :: thesis: ex x being set st
( x in rng F & not F " {x} is finite )
assume A2: for x being set st x in rng F holds
F " {x} is finite ; :: thesis: contradiction
deffunc H₁( set ) -> set = F " {$1};
consider g being Function such that
A3: ( dom g = rng F & ( for x being set st x in rng F holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();

now

let x be set ; :: thesis: ( x in dom g implies g . x is finite )
assume A4: x in dom g ; :: thesis: g . x is finite
g . x = F " {x} by A3, A4;
hence g . x is finite by A2, A3, A4; :: thesis: verum

end;

then A5: Union g is finite by A1, A3, CARD_3:134;
A6: dom F c= Union g

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom F or x in Union g )
assume A7: x in dom F ; :: thesis: x in Union g
( F . x in {(F . x)} & F . x in rng F ) by A7, FUNCT_1:def 5, TARSKI:def 1;
then ( x in F " {(F . x)} & g . (F . x) = F " {(F . x)} & g . (F . x) in rng g ) by A3, A7, FUNCT_1:def 5, FUNCT_1:def 13;
then x in union (rng g) by TARSKI:def 4;
hence x in Union g by CARD_3:def 4; :: thesis: verum

end;

thus contradiction by A1, A5, A6; :: thesis: verum