let i, I be set ; 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; 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; 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; ( 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
; 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); 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
;
i in dom X
by A2, PARTFUN1:def 2;
then
i in (dom P) /\ (dom X)
by A4, XBOOLE_0:def 4;
then A7:
i in dom (P .. X)
by PRALG_1:def 19;
i in dom P
by A2, PARTFUN1:def 2;
then
i in (dom P) /\ (dom (P .. X))
by A7, XBOOLE_0:def 4;
then B1:
i in dom (P .. (P .. X))
by PRALG_1:def 19;
thus f . x =
(P .. X) . i
by A6, A3, PRALG_1:def 19, A7
.=
(P .. (P .. X)) . i
by A1, A5
.=
f . ((P .. X) . i)
by B1, A3, PRALG_1:def 19
.=
f . (f . x)
by A3, A6, A7, PRALG_1:def 19
; verum