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