:: 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
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
{{}} is finite 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
F₁() is set
F₂() is Relation-like non-empty F₁() -defined Function-like total set
F₃() is Relation-like F₁() -defined Function-like total set
S is Relation-like F₁() -defined Function-like total set
D is set
F₂() . D is set
F₃() . D is set
M is set
D .--> M is Relation-like {D} -defined Function-like one-to-one finite set
{D} is finite set
{D} --> M is Relation-like {D} -defined {M} -valued Function-like constant total V21({D},{M}) finite Element of K10(K11({D},{M}))
{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 is Relation-like F₁() -defined Function-like total set
F . D is set
(D .--> M) . D is set
I is set
F . I is set
F₂() . I is set
S . I is set
S is non empty set
D is set
M is set
{ b₁ where b₁ is Element of S : M c= b₁ } is set
{ b₁ where b₁ is Element of S : D c= b₁ } is set
F is set
I is Element of S
I is Element of S
S is set
D is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total set
F is set
D . F is set
S is set
D is Relation-like S -defined Function-like total Function-yielding V25() set
M is Relation-like S -defined Function-like total set
D .. M is Relation-like S -defined Function-like total set
F is Relation-like S -defined Function-like set
S is set
D is Relation-like non-empty S -defined Function-like total set
M is Relation-like non-empty S -defined Function-like total set
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,M
I is Relation-like S -defined Function-like total Element of D
F .. I is Relation-like S -defined Function-like total set
X1 is set
(F .. I) . X1 is set
M . X1 is set
F . X1 is Relation-like Function-like set
i is Relation-like Function-like 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
D is Relation-like non-empty S -defined Function-like total set
M is Relation-like non-empty S -defined Function-like total set
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,M
I is Relation-like S -defined Function-like total Element of D
F .. I is Relation-like S -defined Function-like total set
S is set
D is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total set
F is Relation-like non-empty S -defined Function-like total set
I is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,F
I .. M is Relation-like S -defined Function-like total set
X1 is set
(I .. M) . X1 is set
F . X1 is set
I . X1 is Relation-like Function-like set
i is Relation-like Function-like 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
M is Relation-like S -defined Function-like total Function-yielding V25() set
doms M is Relation-like S -defined Function-like total set
D is Relation-like S -defined Function-like total Function-yielding V25() set
D ** M is Relation-like Function-like Function-yielding V25() set
dom D is set
dom M is set
F is Relation-like S -defined Function-like total Function-yielding V25() set
dom F is set
I is Relation-like S -defined Function-like total set
M .. I is Relation-like S -defined Function-like total set
D .. (M .. I) is Relation-like S -defined Function-like total set
(D ** M) .. I is Relation-like Function-like set
X1 is set
D . X1 is Relation-like Function-like set
M . X1 is Relation-like Function-like set
(D ** M) . X1 is Relation-like Function-like set
f 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 is Relation-like Function-like set
i . (f . (I . X1)) is set
f * i is Relation-like Function-like set
(f * i) . (I . X1) is set
Fi is Relation-like Function-like set
Fi . (I . X1) is set
((D ** M) .. I) . X1 is set
F .. I is Relation-like S -defined Function-like total set
S is set
D is Relation-like S -defined Function-like total Function-yielding V25() set
doms D is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total set
F is Relation-like S -defined Function-like total set
D .. M is Relation-like S -defined Function-like total set
D .. F is Relation-like S -defined Function-like total set
I is set
D . I is Relation-like Function-like set
X1 is Relation-like Function-like 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
D is Relation-like S -defined Function-like total Function-yielding V25() set
doms D is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total set
F is set
dom D is set
D . F is Relation-like Function-like set
I is Relation-like Function-like set
X1 is set
dom I is set
i is set
I . X1 is set
I . i is set
F .--> X1 is Relation-like {F} -defined Function-like one-to-one finite 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 is Relation-like S -defined Function-like total 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
F .--> i is Relation-like {F} -defined Function-like one-to-one finite set
{F} --> i is Relation-like {F} -defined {i} -valued Function-like constant total V21({F},{i}) finite Element of K10(K11({F},{i}))
{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 is Relation-like S -defined Function-like total 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 is Relation-like S -defined Function-like total set
(D .. f) . x is set
Fi . x is set
I . (Fi . x) is set
D .. Fi is Relation-like S -defined Function-like total set
(D .. Fi) . x is set
Fi . x is set
M . x is set
D . x is Relation-like Function-like set
D .. f is Relation-like S -defined Function-like total set
(D .. f) . x is set
X is Relation-like Function-like set
f . x is set
X . (f . x) is set
X . (Fi . x) is set
D .. Fi is Relation-like S -defined Function-like total set
(D .. Fi) . x is set
D .. f is Relation-like S -defined Function-like total set
D .. Fi is Relation-like S -defined Function-like total set
D .. f is Relation-like S -defined Function-like total set
D .. Fi is Relation-like S -defined Function-like total set
S is set
D is Relation-like non-empty S -defined Function-like total set
M is Relation-like non-empty S -defined Function-like total set
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,M
I is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,M
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
F . X1 is Relation-like Function-like set
I . X1 is Relation-like Function-like set
dom I is set
Fi is Relation-like S -defined Function-like total set
x is set
X1 .--> x is Relation-like {X1} -defined Function-like one-to-one finite 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 is Relation-like S -defined Function-like total 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
F .. X is Relation-like S -defined Function-like total set
I .. X is Relation-like S -defined Function-like total 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
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
[[0]] S is Relation-like empty-yielding S -defined Function-like total finite-yielding set
S --> {} is Relation-like S -defined {{}} -valued Function-like constant total V21(S,{{}}) Element of K10(K11(S,{{}}))
K11(S,{{}}) is Relation-like set
K10(K11(S,{{}})) is non empty set
M is Relation-like S -defined Function-like total Element of bool D
S is set
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Element of bool D
M .. F is Relation-like S -defined Function-like total set
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
S is set
D is Relation-like non-empty S -defined Function-like total set
id D is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,D
M is Relation-like S -defined Function-like total Element of D
(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
(id D) . I is Relation-like Function-like 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 is Relation-like Function-like set
X1 . (M . I) is set
(S,D,D,(id D),M) . I is set
S is set
D is Relation-like non-empty S -defined Function-like total set
id D is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,D
M is Relation-like S -defined Function-like total Element of D
F is Relation-like S -defined Function-like total Element of D
(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
D is Relation-like non-empty S -defined Function-like total set
id D is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,D
M is Relation-like S -defined Function-like total Element of D
F is Relation-like S -defined Function-like total Element of D
M \/ F is Relation-like S -defined Function-like total 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
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
id (bool D) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
M is Relation-like S -defined Function-like total Element of bool D
(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
S --> {} is Relation-like S -defined {{}} -valued Function-like constant total V21(S,{{}}) Element of K10(K11(S,{{}}))
K11(S,{{}}) is Relation-like set
K10(K11(S,{{}})) is non empty set
{I} is finite set
F .--> {I} is Relation-like {F} -defined Function-like one-to-one finite set
{F} is finite set
{F} --> {I} is Relation-like {F} -defined {{I}} -valued Function-like constant total V21({F},{{I}}) finite Element of K10(K11({F},{{I}}))
{{I}} is finite V45() set
K11({F},{{I}}) is Relation-like finite set
K10(K11({F},{{I}})) is non empty finite V45() set
(S --> {}) +* (F .--> {I}) is Relation-like Function-like set
dom ((S --> {}) +* (F .--> {I})) is set
dom (F .--> {I}) is finite set
i is Relation-like S -defined Function-like total 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
(S --> {}) . f is set
D . f is set
f is Relation-like S -defined Function-like total Element of bool D
Fi is set
f . Fi is set
(S --> {}) . Fi is set
Fi is Relation-like S -defined Function-like total finite-yielding Element of bool D
(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
(S --> {}) . x is set
Fi . F is finite set
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
id (bool D) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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
F is Relation-like S -defined Function-like total Element of bool D
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,I) is Relation-like S -defined Function-like total Element of bool D
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,(S,D,M,F)) is Relation-like S -defined Function-like total Element of bool D
F is Relation-like S -defined Function-like total Element of bool D
I is Relation-like S -defined Function-like total Element of bool D
F \/ I is Relation-like S -defined Function-like total set
M .. (F \/ I) is Relation-like S -defined Function-like total 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
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
id (bool D) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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 is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
id (bool D) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Element of bool D
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,I) is Relation-like S -defined Function-like total Element of bool D
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
id (bool D) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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,(S,D,M,F)) is Relation-like S -defined Function-like total Element of bool D
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
id (bool D) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Element of bool D
I is Relation-like S -defined Function-like total Element of bool D
F \/ I is Relation-like S -defined Function-like total set
M .. (F \/ I) is Relation-like S -defined Function-like total 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
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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
bool F is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,F)
K113(S,F) is Relation-like S -defined Function-like total set
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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,(S,D,M,F)) is Relation-like S -defined Function-like total Element of bool D
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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
I is Relation-like S -defined Function-like total Element of bool D
F /\ I is Relation-like S -defined Function-like total set
M .. (F /\ I) is Relation-like S -defined Function-like total set
(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
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Element of bool D
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,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
F \/ I is Relation-like S -defined Function-like total set
M .. (F \/ I) is Relation-like S -defined Function-like total set
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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
I 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
F \ I is Relation-like S -defined Function-like total set
M .. (F \ 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
F \/ I is Relation-like S -defined Function-like total set
M .. (F \/ I) is Relation-like S -defined Function-like total set
(F \ I) \/ 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
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F ** M is Relation-like Function-like Function-yielding V25() set
F ** M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
(S,D,F,M) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
I is Relation-like S -defined Function-like total Element of bool D
(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
doms F is Relation-like S -defined Function-like total set
S is set
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
(S,D,F,M) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
doms F is Relation-like S -defined Function-like total set
I is Relation-like S -defined Function-like total Element of bool D
X1 is Relation-like S -defined Function-like total Element of bool D
(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
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
(S,D,F,M) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
(S,D,M,F) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
I is Relation-like S -defined Function-like total Element of bool D
(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
doms M is Relation-like S -defined Function-like total set
doms F 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,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
D is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
(S,D,F,M) is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
I is Relation-like S -defined Function-like total Element of bool D
X1 is Relation-like S -defined Function-like total Element of bool D
I \/ X1 is Relation-like S -defined Function-like total 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
doms F is Relation-like S -defined Function-like total set
F .. (I \/ 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
D is Relation-like S -defined Function-like total 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
F is Relation-like S -defined Function-like total set
[[0]] S is Relation-like empty-yielding S -defined Function-like total finite-yielding set
S --> {} is Relation-like S -defined {{}} -valued Function-like constant total V21(S,{{}}) Element of K10(K11(S,{{}}))
K11(S,{{}}) is Relation-like set
K10(K11(S,{{}})) is non empty set
I is Element of bool (D . M)
M .--> I is Relation-like {M} -defined bool (D . M) -valued Function-like one-to-one finite set
{M} is finite set
{M} --> I is Relation-like {M} -defined bool (D . M) -valued {I} -valued Function-like constant total V21({M},{I}) finite Element of K10(K11({M},{I}))
{I} is finite set
K11({M},{I}) is Relation-like finite set
K10(K11({M},{I})) is non empty finite V45() set
([[0]] S) +* (M .--> I) is Relation-like Function-like set
dom (M .--> I) is finite set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
K113(S,D) is Relation-like S -defined Function-like total 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
([[0]] S) . X1 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
S is set
D is set
M is Relation-like D -defined Function-like total set
bool M is Relation-like non-empty D -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(D,M)
K113(D,M) is Relation-like D -defined Function-like total 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
F is Relation-like Function-like set
I is Relation-like D -defined Function-like total Function-yielding V25() ManySortedFunction of bool M, bool M
I . S is Relation-like Function-like set
X1 is Element of bool (M . S)
F . X1 is set
[[0]] D is Relation-like empty-yielding D -defined Function-like total finite-yielding set
D --> {} is Relation-like D -defined {{}} -valued Function-like constant total V21(D,{{}}) Element of K10(K11(D,{{}}))
K11(D,{{}}) is Relation-like set
K10(K11(D,{{}})) is non empty set
S .--> X1 is Relation-like {S} -defined bool (M . S) -valued Function-like one-to-one finite 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
([[0]] D) +* (S .--> X1) is Relation-like Function-like set
dom (([[0]] D) +* (S .--> X1)) is set
i is Relation-like D -defined Function-like total set
I .. i is Relation-like D -defined Function-like total 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 is Relation-like D -defined Function-like total set
bool M is Relation-like non-empty D -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(D,M)
K113(D,M) is Relation-like D -defined Function-like total 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
F is Relation-like Function-like set
I is Relation-like D -defined Function-like total Function-yielding V25() ManySortedFunction of bool M, bool M
I . S is Relation-like Function-like set
X1 is Element of bool (M . S)
i is Element of bool (M . S)
F . X1 is set
F . i is set
[[0]] D is Relation-like empty-yielding D -defined Function-like total finite-yielding set
D --> {} is Relation-like D -defined {{}} -valued Function-like constant total V21(D,{{}}) Element of K10(K11(D,{{}}))
K11(D,{{}}) is Relation-like set
K10(K11(D,{{}})) is non empty set
S .--> i is Relation-like {S} -defined bool (M . S) -valued Function-like one-to-one finite set
{S} is finite set
{S} --> i is Relation-like {S} -defined bool (M . S) -valued {i} -valued Function-like constant total V21({S},{i}) finite Element of K10(K11({S},{i}))
{i} is finite set
K11({S},{i}) is Relation-like finite set
K10(K11({S},{i})) is non empty finite V45() set
([[0]] D) +* (S .--> i) is Relation-like Function-like set
dom (([[0]] D) +* (S .--> i)) is set
S .--> X1 is Relation-like {S} -defined bool (M . S) -valued Function-like one-to-one 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
([[0]] D) +* (S .--> X1) is Relation-like Function-like set
dom (([[0]] D) +* (S .--> X1)) is set
dom (S .--> i) is finite set
f is Relation-like D -defined Function-like total set
f . S is set
(S .--> i) . S is set
dom (S .--> X1) is finite set
Fi is Relation-like D -defined Function-like total set
Fi . S is set
(S .--> X1) . S is set
x is set
Fi . x is set
f . x is set
([[0]] D) . x is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
dom I is set
I .. Fi is Relation-like D -defined Function-like total set
I .. f is Relation-like D -defined Function-like total set
(I .. Fi) . S is set
(I .. f) . S is set
F . (Fi . S) is set
S is set
D is set
M is Relation-like D -defined Function-like total set
bool M is Relation-like non-empty D -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(D,M)
K113(D,M) is Relation-like D -defined Function-like total 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
F is Relation-like Function-like set
I is Relation-like D -defined Function-like total Function-yielding V25() ManySortedFunction of bool M, bool M
I . S is Relation-like Function-like set
dom I is set
X1 is Element of bool (M . S)
F . X1 is set
F . (F . X1) is set
[[0]] D is Relation-like empty-yielding D -defined Function-like total finite-yielding set
D --> {} is Relation-like D -defined {{}} -valued Function-like constant total V21(D,{{}}) Element of K10(K11(D,{{}}))
K11(D,{{}}) is Relation-like set
K10(K11(D,{{}})) is non empty set
S .--> X1 is Relation-like {S} -defined bool (M . S) -valued Function-like one-to-one finite 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
([[0]] D) +* (S .--> X1) is Relation-like Function-like set
dom (([[0]] D) +* (S .--> X1)) is set
i is Relation-like D -defined Function-like total set
dom (S .--> X1) is finite set
i . S is set
(S .--> X1) . S is set
I .. i is Relation-like D -defined Function-like total set
(I .. i) . S is set
I .. (I .. i) is Relation-like D -defined Function-like total set
(I .. (I .. i)) . S is set
F . ((I .. i) . S) is set
S is set
D is set
M is Relation-like D -defined Function-like total set
bool M is Relation-like non-empty D -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(D,M)
K113(D,M) is Relation-like D -defined Function-like total 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
F is Relation-like Function-like set
I is Relation-like D -defined Function-like total Function-yielding V25() ManySortedFunction of bool M, bool M
I . S is Relation-like Function-like 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
[[0]] D is Relation-like empty-yielding D -defined Function-like total finite-yielding set
D --> {} is Relation-like D -defined {{}} -valued Function-like constant total V21(D,{{}}) Element of K10(K11(D,{{}}))
K11(D,{{}}) is Relation-like set
K10(K11(D,{{}})) is non empty set
S .--> i is Relation-like {S} -defined bool (M . S) -valued Function-like one-to-one finite set
{S} is finite set
{S} --> i is Relation-like {S} -defined bool (M . S) -valued {i} -valued Function-like constant total V21({S},{i}) finite Element of K10(K11({S},{i}))
{i} is finite set
K11({S},{i}) is Relation-like finite set
K10(K11({S},{i})) is non empty finite V45() set
([[0]] D) +* (S .--> i) is Relation-like Function-like set
dom (([[0]] D) +* (S .--> i)) is set
S .--> X1 is Relation-like {S} -defined bool (M . S) -valued Function-like one-to-one 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
([[0]] D) +* (S .--> X1) is Relation-like Function-like set
dom (([[0]] D) +* (S .--> X1)) is set
dom (S .--> i) is finite set
f is Relation-like D -defined Function-like total set
f . S is set
(S .--> i) . S is set
Fi is Relation-like D -defined Function-like total set
dom (S .--> X1) is finite set
Fi . S is set
(S .--> X1) . S is set
Fi \/ f is Relation-like D -defined Function-like total set
(Fi \/ f) . S is set
F . ((Fi \/ f) . S) is set
I .. (Fi \/ f) is Relation-like D -defined Function-like total set
(I .. (Fi \/ f)) . S is set
I .. Fi is Relation-like D -defined Function-like total set
I .. f is Relation-like D -defined Function-like total 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
bool the Sorts of D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound 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, 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
bool the Sorts of D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound 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, 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 Sorts of D is Relation-like non-empty the carrier of S -defined Function-like total set
the carrier of S is set
bool the Sorts of D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound 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, 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
bool the Sorts of the non-empty many-sorted over S is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113( the carrier of S, the Sorts of the non-empty many-sorted over S)
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
D is Relation-like non-empty the carrier of S -defined Function-like total 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
M is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive properly-lower-bound ManySortedSubset of K113( the carrier of S, the Sorts of D)
(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
M is Relation-like non-empty the carrier of S -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ManySortedSubset of K113( the carrier of S, the Sorts of D)
(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
D is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,D
F is set
M . F is Relation-like Function-like set
D . F is set
I is set
X1 is set
i is set
f is set
Fi is Relation-like Function-like set
dom Fi is set
Fi . f is set
F is Relation-like S -defined Function-like total set
I is set
F . I is set
D . I is set
X1 is set
I is Relation-like S -defined Function-like total ManySortedSubset of D
X1 is set
i is set
I . i is set
M . i is Relation-like Function-like set
f is Relation-like Function-like set
dom f is set
f . X1 is set
doms M is Relation-like S -defined Function-like total set
D . i is set
F is Relation-like S -defined Function-like total ManySortedSubset of D
I is Relation-like S -defined Function-like total ManySortedSubset of D
X1 is set
F . X1 is set
I . X1 is set
i is set
M . X1 is Relation-like Function-like set
f is Relation-like Function-like set
dom f is set
f . i is set
i is set
M . X1 is Relation-like Function-like set
f is Relation-like Function-like set
dom f is set
f . i is set
S is set
D is Relation-like empty-yielding S -defined Function-like total finite-yielding set
M is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,D
(S,D,M) is Relation-like S -defined Function-like total finite-yielding ManySortedSubset of D
F is set
(S,D,M) . F is finite set
I is set
M . F is Relation-like Function-like set
X1 is Relation-like Function-like set
dom X1 is set
X1 . I is set
D . F is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() set
K11({},{}) is Relation-like set
K10(K11({},{})) is non empty set
S is set
D is Relation-like S -defined Function-like total set
M is Relation-like S -defined Function-like total set
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,D
F .. M is Relation-like S -defined Function-like total 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
F . I is Relation-like Function-like 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
doms F is Relation-like S -defined Function-like total set
dom X1 is set
I is set
M . I is set
D . I is set
doms F is Relation-like S -defined Function-like total set
(S,D,F) . I is set
F . I is Relation-like Function-like set
X1 is Relation-like Function-like set
dom X1 is set
X1 . (M . I) is set
I is set
M . I is set
(S,D,F) . I is set
F . I is Relation-like Function-like set
dom F is set
(F .. M) . I is set
X1 is Relation-like Function-like set
dom X1 is set
X1 . (M . I) is set
S is set
D is Relation-like S -defined Function-like total set
id D is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of D,D
(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
(id D) . M is Relation-like Function-like set
I is Relation-like Function-like 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
(id D) . M is Relation-like Function-like 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
D is Relation-like the carrier of S -defined Function-like total set
bool D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113( the carrier of S,D)
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)
meet I is Relation-like the carrier of S -defined Function-like total ManySortedSubset of D
M .. (meet I) is Relation-like the carrier of S -defined Function-like total set
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
M . X1 is Relation-like Function-like 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 . (Intersect f) is set
x is Relation-like Function-like set
dom x is set
x . Fi is set
bool (D . X1) is non empty Element of K10(K10((D . X1)))
S is set
D is Relation-like S -defined Function-like total set
K113(S,D) is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
M is Relation-like non-empty S -defined Function-like total properly-upper-bound ManySortedSubset of K113(S,D)
F is Relation-like S -defined Function-like total Element of bool D
I is Relation-like S -defined Function-like total 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
X1 is Relation-like S -defined Function-like total ManySortedSubset of bool D
i is Relation-like S -defined Function-like total ManySortedSubset of K113(S,D)
f is set
i . f is set
D . f is set
M . f is set
F . f is set
f is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
Fi is Relation-like S -defined Function-like total 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
D is Relation-like S -defined Function-like total set
K113(S,D) is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
M is Relation-like non-empty S -defined Function-like total properly-upper-bound ManySortedSubset of K113(S,D)
F is Relation-like S -defined Function-like total Element of bool D
I is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
X1 is set
M . X1 is set
I . X1 is set
F . X1 is set
i is non empty set
{ b₁ where b₁ is Element of i : F . X1 c= b₁ } is set
f is Relation-like S -defined Function-like total set
Fi is set
X1 .--> Fi is Relation-like {X1} -defined Function-like one-to-one finite 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 is Relation-like S -defined Function-like total 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 .--> Fi is Relation-like {X1} -defined i -valued Function-like one-to-one finite set
{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 is Relation-like S -defined Function-like total 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
D is Relation-like S -defined Function-like total set
K113(S,D) is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
M is Relation-like non-empty S -defined Function-like total properly-upper-bound ManySortedSubset of K113(S,D)
I is Relation-like S -defined Function-like total set
X1 is set
(bool D) . X1 is set
f is set
X1 .--> f is Relation-like {X1} -defined Function-like one-to-one finite 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 is Relation-like S -defined Function-like total 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
x is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
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
{ b₁ where b₁ is Element of Z1 : Fi . X1 c= b₁ } is set
sf1 is Element of K10(K10((D . X1)))
Intersect sf1 is Element of K10((D . X1))
Fi is non empty set
{ b₁ where b₁ is Element of Fi : f c= b₁ } is set
I is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
X1 is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
i is Relation-like S -defined Function-like total Element of bool D
(S,D,X1,i) is Relation-like S -defined Function-like total Element of bool D
f is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
meet f is Relation-like S -defined Function-like total ManySortedSubset of 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
{ b₁ where b₁ is Element of X : i . Fi c= b₁ } 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
X1 . Fi is Relation-like Function-like 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
D is Relation-like S -defined Function-like total set
K113(S,D) is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
M is Relation-like non-empty S -defined Function-like total properly-upper-bound ManySortedSubset of K113(S,D)
F is Relation-like S -defined Function-like total Element of bool D
I is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
(S,D,I,F) is Relation-like S -defined Function-like total Element of bool D
X1 is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
meet X1 is Relation-like S -defined Function-like total ManySortedSubset of D
i is Relation-like S -defined Function-like total set
S is set
D is Relation-like S -defined Function-like total set
K113(S,D) is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
M is Relation-like non-empty S -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ManySortedSubset of K113(S,D)
F is Relation-like S -defined Function-like total Element of bool D
I is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
(S,D,I,F) is Relation-like S -defined Function-like total Element of bool D
X1 is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
meet X1 is Relation-like S -defined Function-like total ManySortedSubset of D
i is Relation-like S -defined Function-like total set
f is Relation-like S -defined Function-like total set
S is set
D is Relation-like S -defined Function-like total set
K113(S,D) is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
M is Relation-like non-empty S -defined Function-like total properly-upper-bound ManySortedSubset of K113(S,D)
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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
X1 is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
meet X1 is Relation-like S -defined Function-like total ManySortedSubset of D
i is Relation-like S -defined Function-like total set
I is Relation-like S -defined Function-like total Element of bool D
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
i is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
f is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
Fi is set
f . Fi is set
i . Fi is set
M . Fi is set
x is non empty set
I . Fi is set
X1 . Fi is set
{ b₁ where b₁ is Element of x : I . Fi c= b₁ } is set
{ b₁ where b₁ is Element of x : X1 . Fi c= b₁ } is set
meet i is Relation-like S -defined Function-like total ManySortedSubset of D
meet f is Relation-like S -defined Function-like total ManySortedSubset of D
S is set
D is Relation-like S -defined Function-like total set
K113(S,D) is Relation-like S -defined Function-like total set
bool D is Relation-like non-empty S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113(S,D)
M is Relation-like non-empty S -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ManySortedSubset of K113(S,D)
F is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of bool D, bool D
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,F,(S,D,F,I)) is Relation-like S -defined Function-like total Element of bool D
X1 is Relation-like non-empty S -defined Function-like total ManySortedSubset of K113(S,D)
meet X1 is Relation-like S -defined Function-like total ManySortedSubset of D
i is Relation-like S -defined Function-like total set
f is Relation-like S -defined Function-like total set
F .. (meet X1) is Relation-like S -defined Function-like total set
S is 1-sorted
the carrier of S is set
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
bool the Sorts of D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound 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
the of D is Relation-like non-empty the carrier of S -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ManySortedSubset of K113( the carrier of S, the Sorts of D)
M is Relation-like the carrier of S -defined Function-like total Function-yielding V25() ManySortedFunction of bool the Sorts of D, bool the Sorts of D
S is 1-sorted
the carrier of S is set
D is Relation-like the carrier of S -defined Function-like total set
bool D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113( the carrier of S,D)
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) ( 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 (S) (S) (S) (S)
X1 is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
F is (S) (S) (S) (S)
(S,D,X1) is (S) (S)
i is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
I is (S) (S) (S) (S)
(S,D,i) is (S) (S)
S is 1-sorted
the carrier of S is set
D is Relation-like the carrier of S -defined Function-like total set
bool D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113( the carrier of S,D)
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) ( the carrier of S,D) ManySortedFunction of bool D, bool D
(S,D,M) is (S) (S) (S) (S)
( 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)
S is 1-sorted
the carrier of S is set
D is Relation-like non-empty the carrier of S -defined Function-like total set
bool D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113( the carrier of S,D)
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) ( the carrier of S,D) ManySortedFunction of bool D, bool D
(S,D,M) is (S) (S) (S) (S) (S)
( 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 non-empty (S) (S)
S is 1-sorted
the carrier of S is set
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
bool the Sorts of D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound 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
the of D is Relation-like non-empty the carrier of S -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ManySortedSubset of K113( the carrier of S, the Sorts of D)
M is Relation-like the carrier of S -defined Function-like total Function-yielding V25() ManySortedFunction of bool the Sorts of D, bool the Sorts of D
F is Relation-like the carrier of S -defined Function-like total Function-yielding V25() ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ManySortedFunction of bool the Sorts of D, bool the Sorts of D
X1 is Relation-like non-empty the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
I is Relation-like the carrier of S -defined Function-like total Element of bool the Sorts of D
( the carrier of S, the Sorts of D,F,I) is Relation-like the carrier of S -defined Function-like total Element of bool the Sorts of D
meet X1 is Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of D
F is Relation-like the carrier of S -defined Function-like total Function-yielding V25() ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ManySortedFunction of bool the Sorts of D, bool the Sorts of D
I is Relation-like the carrier of S -defined Function-like total Function-yielding V25() ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ManySortedFunction of bool the Sorts of D, bool the Sorts of D
X1 is Relation-like the carrier of S -defined Function-like total set
i is Relation-like non-empty the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
F .. X1 is Relation-like the carrier of S -defined Function-like total set
meet i is Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of D
I .. X1 is Relation-like the carrier of S -defined Function-like total set
S is 1-sorted
the carrier of S is set
D is Relation-like the carrier of S -defined Function-like total set
bool D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113( the carrier of S,D)
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) ( the carrier of S,D) ManySortedFunction of bool D, bool D
(S,D,M) is (S) (S) (S) (S) (S)
(S,(S,D,M)) is Relation-like the carrier of S -defined Function-like total Function-yielding V25() ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ( the carrier of S, the Sorts of (S,D,M)) ManySortedFunction of bool the Sorts of (S,D,M), bool the Sorts of (S,D,M)
the Sorts of (S,D,M) is Relation-like the carrier of S -defined Function-like total set
bool the Sorts of (S,D,M) is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of K113( the carrier of S, the Sorts of (S,D,M))
K113( the carrier of S, the Sorts of (S,D,M)) is Relation-like the carrier of S -defined Function-like total set
( the carrier of S,(bool D),M) is Relation-like the carrier of S -defined Function-like total ManySortedSubset of bool D
i is Relation-like the carrier of S -defined Function-like total set
(S,(S,D,M)) .. i is Relation-like the carrier of S -defined Function-like total set
M .. i is Relation-like the carrier of S -defined Function-like total set
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)
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)
f is Relation-like non-empty the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of (S,D,M))
dom M is set
Fi 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
M . Fi is Relation-like Function-like set
D . Fi is set
bool (D . Fi) is non empty Element of K10(K10((D . Fi)))
K10((D . Fi)) is non empty set
K10(K10((D . Fi))) is non empty set
K11((bool (D . Fi)),(bool (D . Fi))) is non empty 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)))
i . Fi is set
X is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
(S,D,X) is (S) (S)
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))))
X . (i . Fi) is set
( the carrier of S,(bool D),M) . Fi is set
SF is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
(S,D,SF) is (S) (S)
the Sorts of (S,D,M) . Fi is set
K10(( the Sorts of (S,D,M) . Fi)) is non empty set
K10(K10(( the Sorts of (S,D,M) . Fi))) is non empty set
f . Fi is set
meet f is Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of (S,D,M)
(meet f) . Fi is set
SF is Element of K10(K10(( the Sorts of (S,D,M) . Fi)))
Intersect SF is Element of K10(( the Sorts of (S,D,M) . Fi))
X is non empty set
{ b₁ where b₁ is Element of X : i . Fi c= b₁ } is set
Q is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
(S,D,Q) is (S) (S)
Q is set
Z1 is Element of X
sf1 is Relation-like Function-like set
dom sf1 is set
sf1 . Z1 is set
dom X is set
X . (X . (i . Fi)) is set
((S,(S,D,M)) .. i) . Fi is set
(M .. i) . Fi is set
Q is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
(S,D,Q) is (S) (S)
i is Relation-like the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S,D)
(S,D,i) is (S) (S)
S is 1-sorted
D is (S) (S) (S) (S)
the Sorts of D is Relation-like the carrier of S -defined Function-like total set
the carrier of S is set
(S,D) is Relation-like the carrier of S -defined Function-like total Function-yielding V25() ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ManySortedFunction of bool the Sorts of D, bool the Sorts of D
bool the Sorts of D is Relation-like non-empty the carrier of S -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound 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, the Sorts of D,(S,D)) is (S) (S) (S) (S) (S)
the of D is Relation-like non-empty the carrier of S -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ManySortedSubset of K113( the carrier of S, the Sorts of D)
(S, the Sorts of D, the of D) is (S) (S) (S) (S) (S)
X1 is Relation-like the carrier of S -defined Function-like total set
( the carrier of S,(bool the Sorts of D),(S,D)) is Relation-like the carrier of S -defined Function-like total ManySortedSubset of bool the Sorts of D
dom (S,D) is set
i is set
the of D . i is set
( the carrier of S,(bool the Sorts of D),(S,D)) . i is set
(bool the Sorts of D) . i is set
K11(((bool the Sorts of D) . i),((bool the Sorts of D) . i)) is Relation-like set
K10(K11(((bool the Sorts of D) . i),((bool the Sorts of D) . i))) is non empty set
(S,D) . i is Relation-like Function-like set
x is set
i .--> x is Relation-like {i} -defined Function-like one-to-one finite set
{i} is finite set
{i} --> x is Relation-like {i} -defined {x} -valued Function-like constant total V21({i},{x}) finite Element of K10(K11({i},{x}))
{x} is finite set
K11({i},{x}) is Relation-like finite set
K10(K11({i},{x})) is non empty finite V45() set
X1 +* (i .--> x) is Relation-like Function-like set
dom (X1 +* (i .--> x)) is set
dom (i .--> x) is finite set
f is Relation-like (bool the Sorts of D) . i -defined (bool the Sorts of D) . i -valued Function-like V21((bool the Sorts of D) . i,(bool the Sorts of D) . i) Element of K10(K11(((bool the Sorts of D) . i),((bool the Sorts of D) . i)))
dom f is set
X is Relation-like the carrier of S -defined Function-like total set
X . i is set
(i .--> x) . i is set
X is set
X . X is set
(bool the Sorts of D) . X is set
X1 . X is set
X is Relation-like the carrier of S -defined Function-like total Element of bool the Sorts of D
SF is Relation-like non-empty the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
the Sorts of D . i is set
K10(( the Sorts of D . i)) is non empty set
K10(K10(( the Sorts of D . i))) is non empty set
SF . i is set
meet SF is Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of D
(meet SF) . i is set
Q is Element of K10(K10(( the Sorts of D . i)))
Intersect Q is Element of K10(( the Sorts of D . i))
Fi is non empty set
X . i is set
{ b₁ where b₁ is Element of Fi : X . i c= b₁ } is set
Z1 is set
sf1 is Element of Fi
{ b₁ where b₁ is Element of Fi : x c= b₁ } is set
( the carrier of S, the Sorts of D,(S,D),X) is Relation-like the carrier of S -defined Function-like total Element of bool the Sorts of D
f . x is set
x is set
i .--> x is Relation-like {i} -defined Function-like one-to-one finite set
{i} is finite set
{i} --> x is Relation-like {i} -defined {x} -valued Function-like constant total V21({i},{x}) finite Element of K10(K11({i},{x}))
{x} is finite set
K11({i},{x}) is Relation-like finite set
K10(K11({i},{x})) is non empty finite V45() set
X1 +* (i .--> x) is Relation-like Function-like set
dom (X1 +* (i .--> x)) is set
dom (i .--> x) is finite set
X is Relation-like the carrier of S -defined Function-like total set
X . i is set
(i .--> x) . i is set
X is set
X . X is set
(bool the Sorts of D) . X is set
X1 . X is set
X is Relation-like the carrier of S -defined Function-like total Element of bool the Sorts of D
SF is Relation-like non-empty the carrier of S -defined Function-like total ManySortedSubset of K113( the carrier of S, the Sorts of D)
meet SF is Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of D
Q is Relation-like the carrier of S -defined Function-like total set
Z1 is Relation-like the carrier of S -defined Function-like total set
(meet SF) . i is set
( the carrier of S, the Sorts of D,(S,D),X) is Relation-like the carrier of S -defined Function-like total Element of bool the Sorts of D
( the carrier of S, the Sorts of D,(S,D),X) . i is set
Q is Relation-like Function-like set
dom Q is set
Q . x is set