let I be set ; :: thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological
let M be ManySortedSet of I; :: thesis: for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological
let g, h be SetOp of M; :: thesis: ( g is topological & h is topological implies g * h is topological )
assume that
A1: g is topological and
A2: h is topological ; :: thesis: g * h is topological
let X, Y be Element of Bool M; :: according to CLOSURE2:def 13 :: thesis: (g * h) . (X \/ Y) = ((g * h) . X) \/ ((g * h) . Y)
A3: dom h = Bool M by FUNCT_2:def 1;
hence (g * h) . (X \/ Y) = g . (h . (X \/ Y)) by Th11, FUNCT_1:13
.= g . ((h . X) \/ (h . Y)) by A2, Def15
.= (g . (h . X)) \/ (g . (h . Y)) by A1, Def15
.= ((g * h) . X) \/ (g . (h . Y)) by A3, FUNCT_1:13
.= ((g * h) . X) \/ ((g * h) . Y) by A3, FUNCT_1:13 ;
:: thesis: verum