let S be 1-sorted ; :: thesis: for A being ManySortedSet of the carrier of S

for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J

let A be ManySortedSet of the carrier of S; :: thesis: for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J

let J be MSClosureOperator of A; :: thesis: ClSys->ClOp (ClOp->ClSys J) = J

set I = the carrier of S;

set M = the Sorts of (ClOp->ClSys J);

set j = ClSys->ClOp (ClOp->ClSys J);

A1: ex D being MSSubsetFamily of A st

( D = MSFixPoints J & ClOp->ClSys J = MSClosureStr(# A,D #) ) by Def13;

for X being ManySortedSet of the carrier of S st X in bool A holds

(ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X

for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J

let A be ManySortedSet of the carrier of S; :: thesis: for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J

let J be MSClosureOperator of A; :: thesis: ClSys->ClOp (ClOp->ClSys J) = J

set I = the carrier of S;

set M = the Sorts of (ClOp->ClSys J);

set j = ClSys->ClOp (ClOp->ClSys J);

A1: ex D being MSSubsetFamily of A st

( D = MSFixPoints J & ClOp->ClSys J = MSClosureStr(# A,D #) ) by Def13;

for X being ManySortedSet of the carrier of S st X in bool A holds

(ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X

proof

hence
ClSys->ClOp (ClOp->ClSys J) = J
by A1, Th7; :: thesis: verum
let X be ManySortedSet of the carrier of S; :: thesis: ( X in bool A implies (ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X )

assume X in bool A ; :: thesis: (ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X

then A2: X is Element of bool the Sorts of (ClOp->ClSys J) by A1, MSSUBFAM:11;

then consider SF being V8() MSSubsetFamily of the Sorts of (ClOp->ClSys J) such that

A3: for Y being ManySortedSet of the carrier of S holds

( Y in SF iff ( Y in MSFixPoints J & X c= Y ) ) by A1, Th31;

end;assume X in bool A ; :: thesis: (ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X

then A2: X is Element of bool the Sorts of (ClOp->ClSys J) by A1, MSSUBFAM:11;

then consider SF being V8() MSSubsetFamily of the Sorts of (ClOp->ClSys J) such that

A3: for Y being ManySortedSet of the carrier of S holds

( Y in SF iff ( Y in MSFixPoints J & X c= Y ) ) by A1, Th31;

now :: thesis: for i being object st i in the carrier of S holds

((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i

hence
(ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X
; :: thesis: verum((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i

A4:
dom J = the carrier of S
by PARTFUN1:def 2;

let i be object ; :: thesis: ( i in the carrier of S implies ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i )

assume A5: i in the carrier of S ; :: thesis: ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i

reconsider f = J . i as Function of ((bool A) . i),((bool A) . i) by A5, PBOOLE:def 15;

(bool A) . i = bool (A . i) by A5, MBOOLEAN:def 1;

then reconsider f = f as Function of (bool (A . i)),(bool (A . i)) ;

X . i is Element of (bool A) . i by A1, A2, A5, PBOOLE:def 14;

then A6: X . i is Element of bool (A . i) by A5, MBOOLEAN:def 1;

then A7: X . i c= f . (X . i) by A5, Th24;

reconsider Di = (MSFixPoints J) . i as non empty set by A1, A5;

consider Q being Subset-Family of ( the Sorts of (ClOp->ClSys J) . i) such that

A8: Q = SF . i and

A9: (meet SF) . i = Intersect Q by A5, MSSUBFAM:def 1;

A10: SF . i = { z where z is Element of Di : X . i c= z } by A1, A2, A3, A5, Th32;

A14: ( dom f = bool (A . i) & f . (X . i) in bool (A . i) ) by A6, FUNCT_2:5, FUNCT_2:def 1;

f . (f . (X . i)) = f . (X . i) by A5, A6, Th26;

then f . (X . i) is Element of Di by A5, A14, Def12;

then f . (X . i) in { z where z is Element of Di : X . i c= z } by A7;

then Intersect Q c= f . (X . i) by A8, A10, MSSUBFAM:2;

then Intersect Q = f . (X . i) by A13;

hence ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = f . (X . i) by A1, A2, A3, A9, Def14

.= (J .. X) . i by A5, A4, PRALG_1:def 17 ;

:: thesis: verum

end;let i be object ; :: thesis: ( i in the carrier of S implies ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i )

assume A5: i in the carrier of S ; :: thesis: ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i

reconsider f = J . i as Function of ((bool A) . i),((bool A) . i) by A5, PBOOLE:def 15;

(bool A) . i = bool (A . i) by A5, MBOOLEAN:def 1;

then reconsider f = f as Function of (bool (A . i)),(bool (A . i)) ;

X . i is Element of (bool A) . i by A1, A2, A5, PBOOLE:def 14;

then A6: X . i is Element of bool (A . i) by A5, MBOOLEAN:def 1;

then A7: X . i c= f . (X . i) by A5, Th24;

reconsider Di = (MSFixPoints J) . i as non empty set by A1, A5;

consider Q being Subset-Family of ( the Sorts of (ClOp->ClSys J) . i) such that

A8: Q = SF . i and

A9: (meet SF) . i = Intersect Q by A5, MSSUBFAM:def 1;

A10: SF . i = { z where z is Element of Di : X . i c= z } by A1, A2, A3, A5, Th32;

now :: thesis: for x being set st x in Q holds

f . (X . i) c= x

then A13:
f . (X . i) c= Intersect Q
by A5, A8, MSSUBFAM:5;f . (X . i) c= x

let x be set ; :: thesis: ( x in Q implies f . (X . i) c= x )

assume x in Q ; :: thesis: f . (X . i) c= x

then consider x1 being Element of Di such that

A11: ( x1 = x & X . i c= x1 ) by A8, A10;

MSFixPoints J c= bool A by PBOOLE:def 18;

then Di c= (bool A) . i by A5;

then Di c= bool (A . i) by A5, MBOOLEAN:def 1;

then A12: x1 is Element of bool (A . i) ;

ex g being Function st

( g = J . i & x1 in dom g & g . x1 = x1 ) by A5, Def12;

hence f . (X . i) c= x by A5, A6, A11, A12, Th25; :: thesis: verum

end;assume x in Q ; :: thesis: f . (X . i) c= x

then consider x1 being Element of Di such that

A11: ( x1 = x & X . i c= x1 ) by A8, A10;

MSFixPoints J c= bool A by PBOOLE:def 18;

then Di c= (bool A) . i by A5;

then Di c= bool (A . i) by A5, MBOOLEAN:def 1;

then A12: x1 is Element of bool (A . i) ;

ex g being Function st

( g = J . i & x1 in dom g & g . x1 = x1 ) by A5, Def12;

hence f . (X . i) c= x by A5, A6, A11, A12, Th25; :: thesis: verum

A14: ( dom f = bool (A . i) & f . (X . i) in bool (A . i) ) by A6, FUNCT_2:5, FUNCT_2:def 1;

f . (f . (X . i)) = f . (X . i) by A5, A6, Th26;

then f . (X . i) is Element of Di by A5, A14, Def12;

then f . (X . i) in { z where z is Element of Di : X . i c= z } by A7;

then Intersect Q c= f . (X . i) by A8, A10, MSSUBFAM:2;

then Intersect Q = f . (X . i) by A13;

hence ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = f . (X . i) by A1, A2, A3, A9, Def14

.= (J .. X) . i by A5, A4, PRALG_1:def 17 ;

:: thesis: verum