A1: dom IT c= I by RELAT_1:def 18;

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

assume A2: 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

then IT . i in rng IT by FUNCT_1:3;
hence IT . i is finite by A2, Def2; :: 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 A3: 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 2 :: thesis: ( i in rng IT implies i is finite )
assume i in rng IT ; :: thesis: i is finite
then ex x being set st
( x in dom IT & i = IT . x ) by FUNCT_1:def 3;
hence i is finite by A1, A3; :: thesis: verum