hereby :: thesis: ( ( for x being set holds F . x is finite ) implies F is finite-yielding )

assume A1: F is finite-yielding ; :: thesis: for x being set holds F . b₂ is finite
let x be set ; :: thesis: F . b₁ is finite

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

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

then F . x in rng F by FUNCT_1:12;
hence F . x is finite by A1, FINSET_1:def 2; :: thesis: verum

end;

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

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

end;

end;

end;

assume A2: for x being set holds F . x is finite ; :: thesis: F is finite-yielding
let x be set ; :: according to FINSET_1:def 2 :: thesis: ( not x in rng F or x is finite )
assume x in rng F ; :: thesis: x is finite
then ex y being set st
( y in dom F & x = F . y ) by FUNCT_1:def 5;
hence x is finite by A2; :: thesis: verum