let I be set ; :: thesis: for F being ManySortedFunction of I st doms F is V36() holds
rngs F is V36()
let F be ManySortedFunction of I; :: thesis: ( doms F is V36() implies rngs F is V36() )
assume A1: doms F is V36() ; :: thesis: rngs F is V36()
let i be set ; :: 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