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

proof

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 non-empty 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

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

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;

then A13: f . (X . i) c= Intersect Q by A5, A8, MSSUBFAM:5;
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, PRALG_1:def 20 ;
:: thesis: verum

end;

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

end;

hence ClSys->ClOp (ClOp->ClSys J) = J by A1, Th7; :: thesis: verum