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 ;
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 ; :: thesis: verum