let I be set ; :: thesis: 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; :: 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 3 :: thesis: (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 ;
:: thesis: verum