let I be set ; :: thesis: for F being ManySortedFunction of I st doms F is locally-finite holds
rngs F is locally-finite
let F be ManySortedFunction of I; :: thesis: ( doms F is locally-finite implies rngs F is locally-finite )
assume A1: doms F is locally-finite ; :: thesis: rngs F is locally-finite
let i be set ; :: according to PRE_CIRC:def 3 :: 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, A2, PRE_CIRC:def 3;
then dom f is finite by A2, Th14;
then rng f is finite by FINSET_1:26;
hence (rngs F) . i is finite by A2, Th13; :: thesis: verum