let F be Function; :: thesis: ( ( for x being set st x in rng F holds
x is finite ) implies F is finite-yielding )
assume A1: for x being set st x in rng F holds
x is finite ; :: thesis: F is finite-yielding

now

let y be set ; :: thesis: F . b₁ is finite

per cases ( y in dom F or not y in dom F ) ;

suppose y in dom F ; :: thesis: F . b₁ is finite

hence F . y is finite by A1, FUNCT_1:12; :: thesis: verum

end;

suppose not y in dom F ; :: thesis: F . b₁ is finite

hence F . y is finite by FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence F is finite-yielding by CARD_FIN:def 3; :: thesis: verum