let i, I be set ; :: thesis: for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds

for x being Element of bool (M . i) holds f . x = f . (f . x)

let M be ManySortedSet of I; :: thesis: for f being Function

for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds

for x being Element of bool (M . i) holds f . x = f . (f . x)

let f be Function; :: thesis: for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds

for x being Element of bool (M . i) holds f . x = f . (f . x)

let P be MSSetOp of M; :: thesis: ( P is idempotent & i in I & f = P . i implies for x being Element of bool (M . i) holds f . x = f . (f . x) )

assume that

A1: P is idempotent and

A2: i in I and

A3: f = P . i ; :: thesis: for x being Element of bool (M . i) holds f . x = f . (f . x)

A4: i in dom P by A2, PARTFUN1:def 2;

let x be Element of bool (M . i); :: thesis: f . x = f . (f . x)

dom ((EmptyMS I) +* (i .--> x)) = I by A2, PZFMISC1:1;

then reconsider X = (EmptyMS I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

A5: X is Element of bool M by Lm2, MSSUBFAM:11;

( dom (i .--> x) = {i} & i in {i} ) by TARSKI:def 1;

then A6: X . i = (i .--> x) . i by FUNCT_4:13

.= x by FUNCOP_1:72 ;

hence f . x = (P .. X) . i by A3, A4, PRALG_1:def 17

.= (P .. (P .. X)) . i by A1, A5

.= f . ((P .. X) . i) by A3, A4, PRALG_1:def 17

.= f . (f . x) by A3, A6, A4, PRALG_1:def 17 ;

:: thesis: verum

for f being Function

for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds

for x being Element of bool (M . i) holds f . x = f . (f . x)

let M be ManySortedSet of I; :: thesis: for f being Function

for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds

for x being Element of bool (M . i) holds f . x = f . (f . x)

let f be Function; :: thesis: for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds

for x being Element of bool (M . i) holds f . x = f . (f . x)

let P be MSSetOp of M; :: thesis: ( P is idempotent & i in I & f = P . i implies for x being Element of bool (M . i) holds f . x = f . (f . x) )

assume that

A1: P is idempotent and

A2: i in I and

A3: f = P . i ; :: thesis: for x being Element of bool (M . i) holds f . x = f . (f . x)

A4: i in dom P by A2, PARTFUN1:def 2;

let x be Element of bool (M . i); :: thesis: f . x = f . (f . x)

dom ((EmptyMS I) +* (i .--> x)) = I by A2, PZFMISC1:1;

then reconsider X = (EmptyMS I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

A5: X is Element of bool M by Lm2, MSSUBFAM:11;

( dom (i .--> x) = {i} & i in {i} ) by TARSKI:def 1;

then A6: X . i = (i .--> x) . i by FUNCT_4:13

.= x by FUNCOP_1:72 ;

hence f . x = (P .. X) . i by A3, A4, PRALG_1:def 17

.= (P .. (P .. X)) . i by A1, A5

.= f . ((P .. X) . i) by A3, A4, PRALG_1:def 17

.= f . (f . x) by A3, A6, A4, PRALG_1:def 17 ;

:: thesis: verum