let i be set ; :: according to PRE_CIRC:def 3 :: 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: (MSFuncs A,B) . i = Funcs (A . i),(B . i) by PBOOLE:def 22;
( A . i is finite & B . i is finite ) by A1, PRE_CIRC:def 3;
hence (MSFuncs A,B) . i is finite by A2, FRAENKEL:16; :: thesis: verum