hereby :: thesis: ( ( for i being set st i in I holds
IT . i is finite ) implies IT is finite-yielding )

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

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

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

hence IT . i is finite by A1, Def4; :: thesis: verum

end;

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

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

end;

end;

end;

assume A2: for i being set st i in I holds
IT . i is finite ; :: thesis: IT is finite-yielding
let i be set ; :: according to FINSET_1:def 4 :: thesis: ( i in dom IT implies IT . i is finite )
dom IT c= I ;
hence ( i in dom IT implies IT . i is finite ) by A2; :: thesis: verum