let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or (MSFuncs (A,B)) . i is finite )
assume A1: i in I ; :: thesis: (MSFuncs (A,B)) . i is finite
then A2: B . i is finite by Lm1;
( (MSFuncs (A,B)) . i = Funcs ((A . i),(B . i)) & A . i is finite ) by A1, Lm1, PBOOLE:def 17;
hence (MSFuncs (A,B)) . i is finite by A2, FRAENKEL:6; :: thesis: verum