let I be set ; :: thesis: for M being ManySortedSet of
for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent
let M be ManySortedSet of ; :: thesis: for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent
let g, h be SetOp of M; :: thesis: ( g is idempotent & h is idempotent & g * h = h * g implies g * h is idempotent )
assume that
A1: g is idempotent and
A2: h is idempotent and
A3: g * h = h * g ; :: thesis: g * h is idempotent
let X be Element of Bool M; :: according to CLOSURE2:def 14 :: thesis: (g * h) . X = (g * h) . ((g * h) . X)
A4: dom h = Bool M by FUNCT_2:def 1;
A5: dom g = Bool M by FUNCT_2:def 1;
thus (g * h) . X = g . (h . X) by A4, FUNCT_1:23
.= g . (h . (h . X)) by A2, Def14
.= g . (g . (h . (h . X))) by A1, Def14
.= g . ((h * g) . (h . X)) by A3, A4, FUNCT_1:23
.= g . (h . (g . (h . X))) by A5, FUNCT_1:23
.= g . (h . ((g * h) . X)) by A4, FUNCT_1:23
.= (g * h) . ((g * h) . X) by A4, FUNCT_1:23 ; :: thesis: verum