:: CLOSURE1 semantic presentation

K165() is Element of K10(K161())
K161() is set
K10(K161()) is non empty set
K132() is set
K10(K132()) is non empty set
K10(K165()) is non empty set
K210() is set
{} is set

K188() is M12()
K11(K188(),) is Relation-like set
K10(K11(K188(),)) is non empty set
PFuncs (K188(),) is set
1 is non empty set
F1() is set

F3() is Relation-like F1() -defined Function-like total set

D is set
F2() . D is set
F3() . D is set
M is set

{D} is finite set

{M} is finite set
K11({D},{M}) is Relation-like finite set
K10(K11({D},{M})) is non empty finite V45() set
S +* (D .--> M) is Relation-like Function-like set
dom (S +* (D .--> M)) is set
dom (D .--> M) is finite set

F . D is set
(D .--> M) . D is set
I is set
F . I is set
F2() . I is set
S . I is set
S is non empty set
D is set
M is set
{ b1 where b1 is Element of S : M c= b1 } is set
{ b1 where b1 is Element of S : D c= b1 } is set
F is set
I is Element of S
I is Element of S
S is set

F is set
D . F is set
S is set

S is set

X1 is set
(F .. I) . X1 is set
M . X1 is set

D . X1 is set
K11((D . X1),(M . X1)) is Relation-like set
K10(K11((D . X1),(M . X1))) is non empty set
I . X1 is set
dom F is set
i . (I . X1) is set
S is set

S is set

X1 is set
(I .. M) . X1 is set
F . X1 is set

D . X1 is set
K11((D . X1),(F . X1)) is Relation-like set
K10(K11((D . X1),(F . X1))) is non empty set
M . X1 is set
dom I is set
i . (M . X1) is set
S is set

dom D is set
dom M is set

dom F is set

(D ** M) .. I is Relation-like Function-like set
X1 is set

(D ** M) . X1 is Relation-like Function-like set

dom f is set
(doms M) . X1 is set
I . X1 is set
(M .. I) . X1 is set
f . (I . X1) is set
(D .. (M .. I)) . X1 is set

i . (f . (I . X1)) is set

(f * i) . (I . X1) is set

Fi . (I . X1) is set
((D ** M) .. I) . X1 is set

S is set

I is set

dom X1 is set
(doms D) . I is set
M . I is set
F . I is set
dom D is set
X1 . (M . I) is set
(D .. M) . I is set
X1 . (F . I) is set
S is set

F is set
dom D is set

X1 is set
dom I is set
i is set
I . X1 is set
I . i is set

{F} is finite set
{F} --> X1 is Relation-like {F} -defined {X1} -valued Function-like constant total V21({F},{X1}) finite Element of K10(K11({F},{X1}))
{X1} is finite set
K11({F},{X1}) is Relation-like finite set
K10(K11({F},{X1})) is non empty finite V45() set
M +* (F .--> X1) is Relation-like Function-like set
dom (M +* (F .--> X1)) is set
dom (F .--> X1) is finite set

f . F is set
(F .--> X1) . F is set
Fi is set
f . Fi is set
(doms D) . Fi is set
M . Fi is set

{i} is finite set
K11({F},{i}) is Relation-like finite set
K10(K11({F},{i})) is non empty finite V45() set
M +* (F .--> i) is Relation-like Function-like set
dom (M +* (F .--> i)) is set
dom (F .--> i) is finite set

Fi . F is set
(F .--> i) . F is set
x is set
Fi . x is set
(doms D) . x is set
M . x is set
x is set

(D .. f) . x is set
Fi . x is set
I . (Fi . x) is set

(D .. Fi) . x is set
Fi . x is set
M . x is set

(D .. f) . x is set

f . x is set
X . (f . x) is set
X . (Fi . x) is set

(D .. Fi) . x is set

S is set

X1 is set
D . X1 is set
M . X1 is set
K11((D . X1),(M . X1)) is Relation-like set
K10(K11((D . X1),(M . X1))) is non empty set

dom I is set

x is set

{X1} is finite set
{X1} --> x is Relation-like {X1} -defined {x} -valued Function-like constant total V21({X1},{x}) finite Element of K10(K11({X1},{x}))
{x} is finite set
K11({X1},{x}) is Relation-like finite set
K10(K11({X1},{x})) is non empty finite V45() set
Fi +* (X1 .--> x) is Relation-like Function-like set
dom (Fi +* (X1 .--> x)) is set
dom (X1 .--> x) is finite set

X . X1 is set
(X1 .--> x) . X1 is set
X is set
X . X is set
D . X is set
Fi . X is set

dom F is set
i is Relation-like D . X1 -defined M . X1 -valued Function-like V21(D . X1,M . X1) Element of K10(K11((D . X1),(M . X1)))
i . x is set
(F .. X) . X1 is set
f is Relation-like D . X1 -defined M . X1 -valued Function-like V21(D . X1,M . X1) Element of K10(K11((D . X1),(M . X1)))
f . x is set
S is set

K11(S,) is Relation-like set
K10(K11(S,)) is non empty set

S is set
S is set

S is set

S is set

(S,D,D,(id D),M) is Relation-like S -defined Function-like total Element of D
dom (id D) is set
I is set

M . I is set
D . I is set
id (D . I) is Relation-like D . I -defined D . I -valued Function-like one-to-one total Element of K10(K11((D . I),(D . I)))
K11((D . I),(D . I)) is Relation-like set
K10(K11((D . I),(D . I))) is non empty set

X1 . (M . I) is set
(S,D,D,(id D),M) . I is set
S is set

(S,D,D,(id D),M) is Relation-like S -defined Function-like total Element of D
(S,D,D,(id D),F) is Relation-like S -defined Function-like total Element of D
S is set

(id D) .. (M \/ F) is Relation-like S -defined Function-like total set
(S,D,D,(id D),M) is Relation-like S -defined Function-like total Element of D
(S,D,D,(id D),F) is Relation-like S -defined Function-like total Element of D
(S,D,D,(id D),M) \/ (S,D,D,(id D),F) is Relation-like S -defined Function-like total set
(S,D,D,(id D),M) \/ F is Relation-like S -defined Function-like total set
S is set

(S,D,(id (bool D)),M) is Relation-like S -defined Function-like total Element of bool D
F is set
I is set
(S,D,(id (bool D)),M) . F is set
M . F is set

K11(S,) is Relation-like set
K10(K11(S,)) is non empty set
{I} is finite set

{F} is finite set

{{I}} is finite V45() set
K11({F},{{I}}) is Relation-like finite set
K10(K11({F},{{I}})) is non empty finite V45() set
() +* (F .--> {I}) is Relation-like Function-like set
dom (() +* (F .--> {I})) is set
dom (F .--> {I}) is finite set

i . F is set
(F .--> {I}) . F is set
D . F is set
f is set
i . f is set
(bool D) . f is set
D . f is set
() . f is set
D . f is set

Fi is set
f . Fi is set
() . Fi is set

(S,D,(id (bool D)),Fi) is Relation-like S -defined Function-like total Element of bool D
(S,D,(id (bool D)),Fi) . F is set
x is set
Fi . x is finite set
M . x is set
() . x is set
Fi . F is finite set
S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,I) is Relation-like S -defined Function-like total Element of bool D

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like total Element of bool D

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,F) \/ (S,D,M,I) is Relation-like S -defined Function-like total set
S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,I) is Relation-like S -defined Function-like total Element of bool D
S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like total Element of bool D
S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,F) \/ (S,D,M,I) is Relation-like S -defined Function-like total set
S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D

S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like total Element of bool D
S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D

(S,D,M,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,F) /\ (S,D,M,I) is Relation-like S -defined Function-like total set
S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,F) \/ (S,D,M,I) is Relation-like S -defined Function-like total set

S is set

(S,D,M,F) is Relation-like S -defined Function-like total Element of bool D

(S,D,M,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,F) \ (S,D,M,I) is Relation-like S -defined Function-like total set

(S,D,M,F) \/ (S,D,M,I) is Relation-like S -defined Function-like total set

M .. ((F \ I) \/ I) is Relation-like S -defined Function-like total set
(M .. (F \ I)) \/ (S,D,M,I) is Relation-like S -defined Function-like total set
((M .. (F \ I)) \/ (S,D,M,I)) \ (S,D,M,I) is Relation-like S -defined Function-like total set
(M .. (F \ I)) \ (S,D,M,I) is Relation-like S -defined Function-like total set
S is set

S is set

(S,D,(S,D,F,M),I) is Relation-like S -defined Function-like total Element of bool D
(S,D,F,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,I)) is Relation-like S -defined Function-like total Element of bool D

S is set

(S,D,(S,D,F,M),I) is Relation-like S -defined Function-like total Element of bool D
(S,D,(S,D,F,M),X1) is Relation-like S -defined Function-like total Element of bool D
(S,D,F,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,F,X1) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,I)) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,X1)) is Relation-like S -defined Function-like total Element of bool D
S is set

(S,D,(S,D,F,M),I) is Relation-like S -defined Function-like total Element of bool D
(S,D,(S,D,F,M),(S,D,(S,D,F,M),I)) is Relation-like S -defined Function-like total Element of bool D

(S,D,F,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,I)) is Relation-like S -defined Function-like total Element of bool D
(S,D,F,(S,D,F,I)) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,(S,D,F,I))) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,M,(S,D,F,(S,D,F,I)))) is Relation-like S -defined Function-like total Element of bool D
(S,D,(S,D,M,F),(S,D,F,I)) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,(S,D,M,F),(S,D,F,I))) is Relation-like S -defined Function-like total Element of bool D
(S,D,F,(S,D,M,(S,D,F,I))) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,(S,D,M,(S,D,F,I)))) is Relation-like S -defined Function-like total Element of bool D
(S,D,F,(S,D,(S,D,F,M),I)) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,(S,D,(S,D,F,M),I))) is Relation-like S -defined Function-like total Element of bool D
S is set

(S,D,F,M) .. (I \/ X1) is Relation-like S -defined Function-like total set
(S,D,(S,D,F,M),I) is Relation-like S -defined Function-like total Element of bool D
(S,D,(S,D,F,M),X1) is Relation-like S -defined Function-like total Element of bool D
(S,D,(S,D,F,M),I) \/ (S,D,(S,D,F,M),X1) is Relation-like S -defined Function-like total set

M .. (F .. (I \/ X1)) is Relation-like S -defined Function-like total set
(S,D,F,I) is Relation-like S -defined Function-like total Element of bool D
(S,D,F,X1) is Relation-like S -defined Function-like total Element of bool D
(S,D,F,I) \/ (S,D,F,X1) is Relation-like S -defined Function-like total set
M .. ((S,D,F,I) \/ (S,D,F,X1)) is Relation-like S -defined Function-like total set
(S,D,M,(S,D,F,I)) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,X1)) is Relation-like S -defined Function-like total Element of bool D
(S,D,M,(S,D,F,I)) \/ (S,D,M,(S,D,F,X1)) is Relation-like S -defined Function-like total set
(S,D,(S,D,F,M),I) \/ (S,D,M,(S,D,F,X1)) is Relation-like S -defined Function-like total set
S is set

M is set
D . M is set
K10((D . M)) is non empty set
bool (D . M) is non empty Element of K10(K10((D . M)))
K10(K10((D . M))) is non empty set

K11(S,) is Relation-like set
K10(K11(S,)) is non empty set
I is Element of bool (D . M)

{M} is finite set

{I} is finite set
K11({M},{I}) is Relation-like finite set
K10(K11({M},{I})) is non empty finite V45() set
() +* (M .--> I) is Relation-like Function-like set
dom (M .--> I) is finite set

X1 is set
F . X1 is set
(bool D) . X1 is set
F . M is set
(M .--> I) . M is set
D . X1 is set
bool (D . X1) is non empty Element of K10(K10((D . X1)))
K10((D . X1)) is non empty set
K10(K10((D . X1))) is non empty set

S is set
D is set

M . S is set
K10((M . S)) is non empty set
bool (M . S) is non empty Element of K10(K10((M . S)))
K10(K10((M . S))) is non empty set

X1 is Element of bool (M . S)
F . X1 is set

K11(D,) is Relation-like set
K10(K11(D,)) is non empty set

{S} is finite set
{S} --> X1 is Relation-like {S} -defined bool (M . S) -valued {X1} -valued Function-like constant total V21({S},{X1}) finite Element of K10(K11({S},{X1}))
{X1} is finite set
K11({S},{X1}) is Relation-like finite set
K10(K11({S},{X1})) is non empty finite V45() set
() +* (S .--> X1) is Relation-like Function-like set
dom (() +* (S .--> X1)) is set

i . S is set
(I .. i) . S is set
dom (S .--> X1) is finite set
(S .--> X1) . S is set
dom I is set
S is set
D is set

M . S is set
K10((M . S)) is non empty set
bool (M . S) is non empty Element of K10(K10((M . S)))
K10(K10((M . S))) is non empty set

X1 is Element of bool (M . S)
i is Element of bool (M . S)
F . X1 is set
F . i is set

K11(D,) is Relation-like set
K10(K11(D,)) is non empty set

{S} is finite set

{i} is finite set
K11({S},{i}) is Relation-like finite set
K10(K11({S},{i})) is non empty finite V45() set
() +* (S .--> i) is Relation-like Function-like set
dom (() +* (S .--> i)) is set

{S} --> X1 is Relation-like {S} -defined bool (M . S) -valued {X1} -valued Function-like constant total V21({S},{X1}) finite Element of K10(K11({S},{X1}))
{X1} is finite set
K11({S},{X1}) is Relation-like finite set
K10(K11({S},{X1})) is non empty finite V45() set
() +* (S .--> X1) is Relation-like Function-like set
dom (() +* (S .--> X1)) is set
dom (S .--> i) is finite set

f . S is set
(S .--> i) . S is set
dom (S .--> X1) is finite set

Fi . S is set
(S .--> X1) . S is set
x is set
Fi . x is set
f . x is set

dom I is set

(I .. Fi) . S is set
(I .. f) . S is set
F . (Fi . S) is set
S is set
D is set

M . S is set
K10((M . S)) is non empty set
bool (M . S) is non empty Element of K10(K10((M . S)))
K10(K10((M . S))) is non empty set

dom I is set
X1 is Element of bool (M . S)
F . X1 is set
F . (F . X1) is set

K11(D,) is Relation-like set
K10(K11(D,)) is non empty set

{S} is finite set
{S} --> X1 is Relation-like {S} -defined bool (M . S) -valued {X1} -valued Function-like constant total V21({S},{X1}) finite Element of K10(K11({S},{X1}))
{X1} is finite set
K11({S},{X1}) is Relation-like finite set
K10(K11({S},{X1})) is non empty finite V45() set
() +* (S .--> X1) is Relation-like Function-like set
dom (() +* (S .--> X1)) is set

dom (S .--> X1) is finite set
i . S is set
(S .--> X1) . S is set

(I .. i) . S is set

(I .. (I .. i)) . S is set
F . ((I .. i) . S) is set
S is set
D is set

M . S is set
K10((M . S)) is non empty set
bool (M . S) is non empty Element of K10(K10((M . S)))
K10(K10((M . S))) is non empty set

dom I is set
X1 is Element of bool (M . S)
i is Element of bool (M . S)
X1 \/ i is Element of K10((M . S))
F . (X1 \/ i) is set
F . X1 is set
F . i is set
(F . X1) \/ (F . i) is set

K11(D,) is Relation-like set
K10(K11(D,)) is non empty set

{S} is finite set

{i} is finite set
K11({S},{i}) is Relation-like finite set
K10(K11({S},{i})) is non empty finite V45() set
() +* (S .--> i) is Relation-like Function-like set
dom (() +* (S .--> i)) is set

{S} --> X1 is Relation-like {S} -defined bool (M . S) -valued {X1} -valued Function-like constant total V21({S},{X1}) finite Element of K10(K11({S},{X1}))
{X1} is finite set
K11({S},{X1}) is Relation-like finite set
K10(K11({S},{X1})) is non empty finite V45() set
() +* (S .--> X1) is Relation-like Function-like set
dom (() +* (S .--> X1)) is set
dom (S .--> i) is finite set

f . S is set
(S .--> i) . S is set

dom (S .--> X1) is finite set
Fi . S is set
(S .--> X1) . S is set

(Fi \/ f) . S is set
F . ((Fi \/ f) . S) is set

(I .. (Fi \/ f)) . S is set

(I .. Fi) \/ (I .. f) is Relation-like D -defined Function-like total set
((I .. Fi) \/ (I .. f)) . S is set
(I .. Fi) . S is set
(I .. f) . S is set
((I .. Fi) . S) \/ ((I .. f) . S) is set
F . (Fi . S) is set
(F . (Fi . S)) \/ ((I .. f) . S) is set
S is 1-sorted
S is 1-sorted
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the carrier of S is set

K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
(S, the Sorts of D,(bool the Sorts of D)) is (S) (S)
S is 1-sorted
D is many-sorted over S
(S,D) is (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the carrier of S is set

K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
(S, the Sorts of D,(bool the Sorts of D)) is (S) (S)
the Sorts of (S,D) is Relation-like the carrier of S -defined Function-like total set
the of (S,D) is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of (S,D))
K113( the carrier of S, the Sorts of (S,D)) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
D is non-empty many-sorted over S
(S,D) is (S) (S) (S) (S) (S) (S) (S) (S)

the carrier of S is set

K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
(S, the Sorts of D,(bool the Sorts of D)) is (S) (S)
S is 1-sorted
the non-empty many-sorted over S is non-empty many-sorted over S
(S, the non-empty many-sorted over S) is non-empty (S) (S) (S) (S) (S) (S) (S) (S)
the Sorts of the non-empty many-sorted over S is Relation-like non-empty the carrier of S -defined Function-like total set
the carrier of S is set

K113( the carrier of S, the Sorts of the non-empty many-sorted over S) is Relation-like the carrier of S -defined Function-like total set
(S, the Sorts of the non-empty many-sorted over S,(bool the Sorts of the non-empty many-sorted over S)) is (S) (S)
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
the carrier of S is set
D is (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
the carrier of S is set

K113( the carrier of S,D) is Relation-like the carrier of S -defined Function-like total set
M is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
(S,D,M) is (S) (S)
the Sorts of (S,D,M) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
M is Relation-like the carrier of S -defined Function-like total additive ManySortedSubset of K113( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set

(S, the Sorts of D,M) is (S) (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
M is Relation-like the carrier of S -defined Function-like total multiplicative ManySortedSubset of K113( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set

(S, the Sorts of D,M) is (S) (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
M is Relation-like non-empty the carrier of S -defined Function-like total properly-upper-bound ManySortedSubset of K113( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S)
S is 1-sorted
the carrier of S is set
D is many-sorted over S
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
M is Relation-like non-empty the carrier of S -defined Function-like total properly-lower-bound ManySortedSubset of K113( the carrier of S, the Sorts of D)
(S, the Sorts of D,M) is (S) (S)
S is 1-sorted
D is (S)
the carrier of S is set
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
D is (S)
the carrier of S is set
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
D is (S)
the carrier of S is set
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
D is (S)
the carrier of S is set
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the of D is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
K113( the carrier of S, the Sorts of D) is Relation-like the carrier of S -defined Function-like total set
S is set
S is set

F is set

D . F is set
I is set
X1 is set
i is set
f is set

dom Fi is set
Fi . f is set

I is set
F . I is set
D . I is set
X1 is set

X1 is set
i is set
I . i is set

dom f is set
f . X1 is set

D . i is set

X1 is set
F . X1 is set
I . X1 is set
i is set

dom f is set
f . i is set
i is set

dom f is set
f . i is set
S is set

F is set
(S,D,M) . F is finite set
I is set

dom X1 is set
X1 . I is set

K11({},{}) is Relation-like set
K10(K11({},{})) is non empty set
S is set

(S,D,F) is Relation-like S -defined Function-like total ManySortedSubset of D
I is set
M . I is set
(S,D,F) . I is set
D . I is set
K11((D . I),(D . I)) is Relation-like set
K10(K11((D . I),(D . I))) is non empty set

dom F is set
X1 is Relation-like D . I -defined D . I -valued Function-like V21(D . I,D . I) Element of K10(K11((D . I),(D . I)))
X1 . (M . I) is set

dom X1 is set
I is set
M . I is set
D . I is set

(S,D,F) . I is set

dom X1 is set
X1 . (M . I) is set
I is set
M . I is set
(S,D,F) . I is set

dom F is set
(F .. M) . I is set

dom X1 is set
X1 . (M . I) is set
S is set

(S,D,(id D)) is Relation-like S -defined Function-like total ManySortedSubset of D
M is set
(S,D,(id D)) . M is set
D . M is set
F is set

dom I is set
I . F is set
K11((D . M),(D . M)) is Relation-like set
K10(K11((D . M),(D . M))) is non empty set
K11((D . M),(D . M)) is Relation-like set
K10(K11((D . M),(D . M))) is non empty set

I is set
F is Relation-like D . M -defined D . M -valued Function-like V21(D . M,D . M) Element of K10(K11((D . M),(D . M)))
dom F is set
id (D . M) is Relation-like D . M -defined D . M -valued Function-like one-to-one total Element of K10(K11((D . M),(D . M)))
F . I is set
S is 1-sorted
the carrier of S is set

K113( the carrier of S,D) is Relation-like the carrier of S -defined Function-like total set
M is Relation-like the carrier of S -defined Function-like total Function-yielding V25() ( the carrier of S,D) ( the carrier of S,D) ManySortedFunction of bool D, bool D
( the carrier of S,(bool D),M) is Relation-like the carrier of S -defined Function-like total ManySortedSubset of bool D
F is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
(S,D,F) is (S) (S)
I is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)

X1 is set
(M .. (meet I)) . X1 is set
(meet I) . X1 is set
(bool D) . X1 is set
K11(((bool D) . X1),((bool D) . X1)) is Relation-like set
K10(K11(((bool D) . X1),((bool D) . X1))) is non empty set

dom M is set
D . X1 is set
K10((D . X1)) is non empty set
K10(K10((D . X1))) is non empty set
I . X1 is set
f is Element of K10(K10((D . X1)))
Intersect f is Element of K10((D . X1))
Fi is set
F . X1 is set
i is Relation-like (bool D) . X1 -defined (bool D) . X1 -valued Function-like V21((bool D) . X1,(bool D) . X1) Element of K10(K11(((bool D) . X1),((bool D) . X1)))
i . () is set

dom x is set
x . Fi is set
bool (D . X1) is non empty Element of K10(K10((D . X1)))
S is set

X1 is set
I . X1 is set
(bool D) . X1 is set
M . X1 is set
D . X1 is set
bool (D . X1) is non empty Element of K10(K10((D . X1)))
K10((D . X1)) is non empty set
K10(K10((D . X1))) is non empty set
i is set

f is set
i . f is set
D . f is set
M . f is set
F . f is set

x is set
Fi . x is set
M . x is set
f . x is set
x is set
F . x is set
Fi . x is set
f . x is set
x is set
Fi . x is set
f . x is set
M . x is set
F . x is set
S is set

X1 is set
M . X1 is set
I . X1 is set
F . X1 is set
i is non empty set
{ b1 where b1 is Element of i : F . X1 c= b1 } is set

Fi is set

{X1} is finite set
{X1} --> Fi is Relation-like {X1} -defined {Fi} -valued Function-like constant total V21({X1},{Fi}) finite Element of K10(K11({X1},{Fi}))
{Fi} is finite set
K11({X1},{Fi}) is Relation-like finite set
K10(K11({X1},{Fi})) is non empty finite V45() set
f +* (X1 .--> Fi) is Relation-like Function-like set
dom (f +* (X1 .--> Fi)) is set
dom (X1 .--> Fi) is finite set

x . X1 is set
(X1 .--> Fi) . X1 is set
X is set
x . X is set
I . X is set
f . X is set
f is set
Fi is Element of i

{X1} is finite set
{X1} --> Fi is Relation-like {X1} -defined i -valued {Fi} -valued Function-like constant total V21({X1},{Fi}) finite Element of K10(K11({X1},{Fi}))
{Fi} is finite set
K11({X1},{Fi}) is Relation-like finite set
K10(K11({X1},{Fi})) is non empty finite V45() set
D +* (X1 .--> Fi) is Relation-like Function-like set
dom (D +* (X1 .--> Fi)) is set
dom (X1 .--> Fi) is finite set

x . X1 is set
(X1 .--> Fi) . X1 is set
X is set
F . X is set
x . X is set
D . X is set
X is set
x . X is set
M . X is set
D . X is set
S is set

X1 is set
(bool D) . X1 is set
f is set

{X1} is finite set
{X1} --> f is Relation-like {X1} -defined {f} -valued Function-like constant total V21({X1},{f}) finite Element of K10(K11({X1},{f}))
{f} is finite set
K11({X1},{f}) is Relation-like finite set
K10(K11({X1},{f})) is non empty finite V45() set
I +* (X1 .--> f) is Relation-like Function-like set
dom (I +* (X1 .--> f)) is set
dom (X1 .--> f) is finite set

Fi . X1 is set
(X1 .--> f) . X1 is set
x is set
Fi . x is set
(bool D) . x is set
I . x is set

D . X1 is set
K10((D . X1)) is non empty set
K10(K10((D . X1))) is non empty set
x . X1 is set
i is non empty set
X is Element of K10(K10((D . X1)))
Intersect X is Element of K10((D . X1))
K11(i,i) is non empty Relation-like set
K10(K11(i,i)) is non empty set
X is Element of i
i --> X is non empty Relation-like i -defined i -valued Function-like constant total V21(i,i) Element of K10(K11(i,i))
{X} is finite set
K11(i,{X}) is Relation-like set
SF is Relation-like i -defined i -valued Function-like V21(i,i) Element of K10(K11(i,i))
SF . f is set
bool (D . X1) is non empty Element of K10(K10((D . X1)))
Q is set
M . X1 is set
Z1 is non empty set
{ b1 where b1 is Element of Z1 : Fi . X1 c= b1 } is set
sf1 is Element of K10(K10((D . X1)))
Intersect sf1 is Element of K10((D . X1))
Fi is non empty set
{ b1 where b1 is Element of Fi : f c= b1 } is set

(S,D,X1,i) is Relation-like S -defined Function-like total Element of bool D

Fi is set
D . Fi is set
K10((D . Fi)) is non empty set
K10(K10((D . Fi))) is non empty set
f . Fi is set
(meet f) . Fi is set
x is Element of K10(K10((D . Fi)))
Intersect x is Element of K10((D . Fi))
M . Fi is set
X is non empty set
i . Fi is set
{ b1 where b1 is Element of X : i . Fi c= b1 } is set
(bool D) . Fi is set
K11(((bool D) . Fi),((bool D) . Fi)) is Relation-like set
K10(K11(((bool D) . Fi),((bool D) . Fi))) is non empty set

X is Relation-like (bool D) . Fi -defined (bool D) . Fi -valued Function-like V21((bool D) . Fi,(bool D) . Fi) Element of K10(K11(((bool D) . Fi),((bool D) . Fi)))
dom X1 is set
(S,D,X1,i) . Fi is set
X . (i . Fi) is set
S is set