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 monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let M be ManySortedSet of I; :: thesis: for f being Function
for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let f be Function; :: thesis: for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let P be MSSetOp of M; :: thesis: ( P is monotonic & i in I & f = P . i implies for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y )
assume that
A1: P is monotonic and
A2: i in I and
A3: f = P . i ; :: thesis: for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let x, y be Element of bool (M . i); :: thesis: ( x c= y implies f . x c= f . y )
assume A4: x c= y ; :: thesis: f . x c= f . y
dom ((EmptyMS I) +* (i .--> y)) = I by A2, PZFMISC1:1;
then reconsider Y = (EmptyMS I) +* (i .--> y) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
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: i in {i} by TARSKI:def 1;
dom (i .--> y) = {i} ;
then A6: Y . i = (i .--> y) . i by A5, FUNCT_4:13
.= y by FUNCOP_1:72 ;
dom (i .--> x) = {i} ;
then A8: X . i = (i .--> x) . i by A5, FUNCT_4:13
.= x by FUNCOP_1:72 ;
A9: X c= Y

proof

let s be object ; :: according to PBOOLE:def 2 :: thesis: ( not s in I or X . s c= Y . s )
assume s in I ; :: thesis: X . s c= Y . s

per cases ( s = i or s <> i ) ;

suppose s = i ; :: thesis: X . s c= Y . s

hence X . s c= Y . s by A4, A8, A6; :: thesis: verum

end;

suppose s <> i ; :: thesis: X . s c= Y . s

then not s in dom (i .--> x) by TARSKI:def 1;
then A10: X . s = (EmptyMS I) . s by FUNCT_4:11;
thus X . s c= Y . s by A10; :: thesis: verum

end;

end;

end;

A11: i in dom P by A2, PARTFUN1:def 2;
( X is Element of bool M & Y is Element of bool M ) by Lm2, MSSUBFAM:11;
then P .. X c= P .. Y by A1, A9;
then A12: (P .. X) . i c= (P .. Y) . i by A2;
i in dom Y by A2, PARTFUN1:def 2;
then i in (dom P) /\ (dom Y) by A11, XBOOLE_0:def 4;
then i in dom (P .. Y) by PRALG_1:def 19;
then W: (P .. Y) . i = f . (Y . i) by PRALG_1:def 19, A3;
dom X = I by PARTFUN1:def 2;
then i in dom X by A2;
then i in (dom P) /\ (dom X) by A11, XBOOLE_0:def 4;
then i in dom (P .. X) by PRALG_1:def 19;
then f . (X . i) = (P .. X) . i by A3, PRALG_1:def 19;
then f . (X . i) c= (P .. Y) . i by A12;
hence f . x c= f . y by A8, A6, W; :: thesis: verum