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