M # is non-empty

proof

let i be set ; :: according to PBOOLE:def 16 :: thesis: ( i in I * implies not (M # ) . i is empty )
assume i in I * ; :: thesis: not (M # ) . i is empty
then reconsider f = i as Element of I * ;
not {} in rng M by Th149;
then not {} in rng (M * f) by FUNCT_1:25;
then product (M * f) <> {} by CARD_3:37;
hence not (M # ) . i is empty by Def19; :: thesis: verum

end;

hence M # is non-empty ; :: thesis: verum