let I be set ; :: thesis: for M being ManySortedSet of I
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 I; :: 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 12 :: thesis: (g * h) . X = (g * h) . ((g * h) . X)
A4: dom g = Bool M by FUNCT_2:def 1;
A5: dom h = Bool M by FUNCT_2:def 1;
hence (g * h) . X = g . (h . X) by FUNCT_1:13
.= g . (h . (h . X)) by A2
.= g . (g . (h . (h . X))) by A1
.= g . ((h * g) . (h . X)) by A3, A5, FUNCT_1:13
.= g . (h . (g . (h . X))) by A4, FUNCT_1:13
.= g . (h . ((g * h) . X)) by A5, FUNCT_1:13
.= (g * h) . ((g * h) . X) by A5, FUNCT_1:13 ;
:: thesis: verum