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 4 :: 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:16;
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
.= (P .. (R .. X)) (\/) (P .. (R .. Y)) by A1
.= ((P ** R) .. X) (\/) (P .. (R .. Y)) by A3, Th4, MSSUBFAM:12
.= ((P ** R) .. X) (\/) ((P ** R) .. Y) by A3, Th4, MSSUBFAM:12 ;
:: thesis: verum