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 22;
hence (MSFuncs A,B) . i is finite by A2, FRAENKEL:16; :: thesis: verum