let I be set ; :: thesis: for F being ManySortedFunction of I st doms F is finite-yielding holds
rngs F is finite-yielding
let F be ManySortedFunction of I; :: thesis: ( doms F is finite-yielding implies rngs F is finite-yielding )
assume A1: doms F is finite-yielding ; :: thesis: rngs F is finite-yielding
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or (rngs F) . i is finite )
assume A2: i in I ; :: thesis: (rngs F) . i is finite
reconsider f = F . i as Function ;
(doms F) . i is finite by A1;
then dom f is finite by A2, Th14;
then rng f is finite by FINSET_1:8;
hence (rngs F) . i is finite by A2, Th13; :: thesis: verum