let I be set ; for M being ManySortedSet of I
for P, R being MSSetOp of M st P is idempotent & R is idempotent & P ** R = R ** P holds
P ** R is idempotent
let M be ManySortedSet of I; for P, R being MSSetOp of M st P is idempotent & R is idempotent & P ** R = R ** P holds
P ** R is idempotent
let P, R be MSSetOp of M; ( P is idempotent & R is idempotent & P ** R = R ** P implies P ** R is idempotent )
assume that
A1:
P is idempotent
and
A2:
R is idempotent
and
A3:
P ** R = R ** P
; P ** R is idempotent
let X be Element of bool M; CLOSURE1:def 3 (P ** R) .. X = (P ** R) .. ((P ** R) .. X)
A4:
doms P = bool M
by MSSUBFAM:17;
A5:
doms R = bool M
by MSSUBFAM:17;
hence (P ** R) .. X =
P .. (R .. X)
by Th4, MSSUBFAM:12
.=
P .. (R .. (R .. X))
by A2
.=
P .. (P .. (R .. (R .. X)))
by A1
.=
P .. ((R ** P) .. (R .. X))
by A3, A5, Th4, MSSUBFAM:12
.=
P .. (R .. (P .. (R .. X)))
by A4, Th4, MSSUBFAM:12
.=
P .. (R .. ((P ** R) .. X))
by A5, Th4, MSSUBFAM:12
.=
(P ** R) .. ((P ** R) .. X)
by A5, Th4, MSSUBFAM:12
;
verum