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

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