for i being set st i in I holds
not (MSFuncs (A,A)) . i is empty

proof

let i be set ; :: thesis: ( i in I implies not (MSFuncs (A,A)) . i is empty )
assume A1: i in I ; :: thesis: not (MSFuncs (A,A)) . i is empty
then (id A) . i is Function of (A . i),(A . i) by PBOOLE:def 18;
then (id A) . i in Funcs ((A . i),(A . i)) by FUNCT_2:12;
hence not (MSFuncs (A,A)) . i is empty by A1, PBOOLE:def 22; :: thesis: verum

end;

hence MSFuncs (A,A) is non-empty by PBOOLE:def 16; :: thesis: verum