let I be set ; :: thesis: for M being ManySortedSet of
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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: P ** R is idempotent
let X be Element of bool M; :: according to CLOSURE1:def 4 :: thesis: (P ** R) .. X = (P ** R) .. ((P ** R) .. X)
A4: doms R = bool M by MSSUBFAM:17;
A5: doms P = bool M by MSSUBFAM:17;
thus (P ** R) .. X = P .. (R .. X) by A4, Th4, MSSUBFAM:12
.= P .. (R .. (R .. X)) by A2, Def4
.= P .. (P .. (R .. (R .. X))) by A1, Def4
.= P .. ((R ** P) .. (R .. X)) by A3, A4, Th4, MSSUBFAM:12
.= P .. (R .. (P .. (R .. X))) by A5, Th4, MSSUBFAM:12
.= P .. (R .. ((P ** R) .. X)) by A4, Th4, MSSUBFAM:12
.= (P ** R) .. ((P ** R) .. X) by A4, Th4, MSSUBFAM:12 ; :: thesis: verum