let I be set ; :: thesis: for M being ManySortedSet of I
for P, R being MSSetOp of M st P is topological & R is topological holds
P ** R is topological
let M be ManySortedSet of I; :: thesis: for P, R being MSSetOp of M st P is topological & R is topological holds
P ** R is topological
let P, R be MSSetOp of M; :: thesis: ( P is topological & R is topological implies P ** R is topological )
assume that
A1: P is topological and
A2: R is topological ; :: thesis: P ** R is topological
let X, Y be Element of bool M; :: according to CLOSURE1:def 5 :: thesis: (P ** R) .. (X \/ Y) = ((P ** R) .. X) \/ ((P ** R) .. Y)
A3: doms R = bool M by MSSUBFAM:17;
Y in bool M by MSSUBFAM:12;
then A4: Y c= M by MBOOLEAN:1;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:1;
then X \/ Y c= M by A4, PBOOLE:18;
then X \/ Y in doms R by A3, MBOOLEAN:1;
hence (P ** R) .. (X \/ Y) = P .. (R .. (X \/ Y)) by Th4
.= P .. ((R .. X) \/ (R .. Y)) by A2, Def5
.= (P .. (R .. X)) \/ (P .. (R .. Y)) by A1, Def5
.= ((P ** R) .. X) \/ (P .. (R .. Y)) by A3, Th4, MSSUBFAM:12
.= ((P ** R) .. X) \/ ((P ** R) .. Y) by A3, Th4, MSSUBFAM:12 ;
:: thesis: verum