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 (([[0]] I) +* (i .--> y)) = I by A2, PZFMISC1:1;
then reconsider Y = ([[0]] I) +* (i .--> y) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
dom (([[0]] I) +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = ([[0]] I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
A5: i in {i} by TARSKI:def 1;
A6: dom (i .--> y) = {i} by FUNCOP_1:19;
then A7: Y . i = (i .--> y) . i by A5, FUNCT_4:14
.= y by FUNCOP_1:87 ;
A8: dom (i .--> x) = {i} by FUNCOP_1:19;
then A9: X . i = (i .--> x) . i by A5, FUNCT_4:14
.= x by FUNCOP_1:87 ;
A10: X c= Y

proof

let s be set ; :: according to PBOOLE:def 5 :: 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, A9, A7; :: thesis: verum

end;

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

then not s in dom (i .--> x) by A8, TARSKI:def 1;
then A12: X . s = ([[0]] I) . s by FUNCT_4:12;
not s in dom (i .--> y) by A6, A11, TARSKI:def 1;
hence X . s c= Y . s by A12, FUNCT_4:12; :: thesis: verum

end;

end;

end;

A13: i in dom P by A2, PARTFUN1:def 4;
( X is Element of bool M & Y is Element of bool M ) by Lm2, MSSUBFAM:11;
then P .. X c= P .. Y by A1, A10, Def3;
then (P .. X) . i c= (P .. Y) . i by A2, PBOOLE:def 5;
then f . (X . i) c= (P .. Y) . i by A3, A13, PRALG_1:def 17;
hence f . x c= f . y by A3, A9, A7, A13, PRALG_1:def 17; :: thesis: verum