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);
consider D being MSSubsetFamily of A such that
A1:
D = MSFixPoints J
and
A2:
ClOp->ClSys J = MSClosureStr(# A,D #)
by Def14;
A3:
the Family of (ClOp->ClSys J) = D
by A2;
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 A4:
X is
Element of
bool the
Sorts of
(ClOp->ClSys J)
by A2, MSSUBFAM:11;
then consider SF being
V8 MSSubsetFamily of the
Sorts of
(ClOp->ClSys J) such that A5:
for
Y being
ManySortedSet of the
carrier of
S holds
(
Y in SF iff (
Y in MSFixPoints J &
X c= Y ) )
by A1, A3, Th31;
now let i be
set ;
:: thesis: ( i in the carrier of S implies ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i )assume A6:
i in the
carrier of
S
;
:: thesis: ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . iA7:
dom J = the
carrier of
S
by PBOOLE:def 3;
reconsider f =
J . i as
Function of
(bool A) . i,
(bool A) . i by A6, PBOOLE:def 18;
(bool A) . i = bool (A . i)
by A6, MBOOLEAN:def 1;
then reconsider f =
f as
Function of
bool (A . i),
bool (A . i) ;
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 A6, MSSUBFAM:def 2;
reconsider Di =
(MSFixPoints J) . i as non
empty set by A1, A3, A6;
Intersect Q = f . (X . i)
proof
A10:
SF . i = { z where z is Element of Di : X . i c= z }
by A1, A3, A4, A5, A6, Th32;
X . i is
Element of
(bool A) . i
by A2, A4, A6, PBOOLE:def 17;
then A11:
X . i is
Element of
bool (A . i)
by A6, MBOOLEAN:def 1;
A12:
dom f = bool (A . i)
by FUNCT_2:def 1;
A13:
f . (X . i) in bool (A . i)
by A11, FUNCT_2:7;
f . (f . (X . i)) = f . (X . i)
by A6, A11, Th26;
then A14:
f . (X . i) is
Element of
Di
by A6, A12, A13, Def13;
X . i c= f . (X . i)
by A6, A11, Th24;
then
f . (X . i) in { z where z is Element of Di : X . i c= z }
by A14;
hence
Intersect Q c= f . (X . i)
by A8, A10, MSSUBFAM:2;
:: according to XBOOLE_0:def 10 :: thesis: f . (X . i) c= Intersect Q
A15:
Q <> {}
by A6, A8;
hence
f . (X . i) c= Intersect Q
by A15, MSSUBFAM:5;
:: thesis: verum
end; hence ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i =
f . (X . i)
by A1, A2, A4, A5, A9, Def15
.=
(J .. X) . i
by A6, A7, PRALG_1:def 17
;
:: thesis: verum end;
hence
(ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X
by PBOOLE:3;
:: thesis: verum
end;
hence
ClSys->ClOp (ClOp->ClSys J) = J
by A2, Th7; :: thesis: verum