hereby :: thesis: ( ( for i being object st i in dom f holds
f . i is finite ) implies f is finite-yielding )

assume A1: f is finite-yielding ; :: thesis: for i being object st i in dom f holds
f . b₂ is finite
let i be object ; :: thesis: ( i in dom f implies f . b₁ is finite )
assume i in dom f ; :: thesis: f . b₁ is finite

per cases ( i in dom f or not i in dom f ) ;

suppose i in dom f ; :: thesis: f . b₁ is finite

then f . i in rng f by FUNCT_1:3;
hence f . i is finite by A1; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: f . b₁ is finite

hence f . i is finite by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

assume A2: for i being object st i in dom f holds
f . i is finite ; :: thesis: f is finite-yielding
let i be set ; :: according to FINSET_1:def 2 :: thesis: ( i in rng f implies i is finite )
assume i in rng f ; :: thesis: i is finite
then ex x being object st
( x in dom f & i = f . x ) by FUNCT_1:def 3;
hence i is finite by A2; :: thesis: verum