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 Th10, FUNCT_1:13
.= g . ((h . X) (\/) (h . Y)) by A2
.= (g . (h . X)) (\/) (g . (h . Y)) by A1
.= ((g * h) . X) (\/) (g . (h . Y)) by A3, FUNCT_1:13
.= ((g * h) . X) (\/) ((g * h) . Y) by A3, FUNCT_1:13 ;
:: thesis: verum