let S be 1-sorted ; 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; for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J
let J be MSClosureOperator of A; 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;
( X in bool A implies (ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X )
assume
X in bool A
;
(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 for i being object st i in the carrier of S holds
((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . ilet i be
object ;
( 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
;
((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . ireconsider 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;
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
;
verum end;
hence
(ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X
;
verum
end;
hence
ClSys->ClOp (ClOp->ClSys J) = J
by A1, Th7; verum