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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom F or x in Union g )
assume A5: x in dom F ; :: thesis: x in Union g
A6: F . x in rng F by A5, FUNCT_1:def 3;
then A7: g . (F . x) in rng g by A3, FUNCT_1:def 3;
F . x in {(F . x)} by TARSKI:def 1;
then A8: x in F " {(F . x)} by A5, FUNCT_1:def 7;
g . (F . x) = F " {(F . x)} by A3, A6;
then x in union (rng g) by A8, A7, TARSKI:def 4;
hence x in Union g ; :: thesis: verum

end;

assume A9: for x being object st x in rng F holds
F " {x} is finite ; :: thesis: contradiction

now :: thesis: for x being object st x in dom g holds
g . x is finite

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

end;

then Union g is finite by A2, A3, Th87;
hence contradiction by A1, A4; :: thesis: verum