:: 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

F

F

S is Relation-like F

D is set

F

F

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

F . D is set

(D .--> M) . D is set

I is set

F . I is set

F

S . I is set

S is non empty set

D is set

M is set

{ b

{ b

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

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

sf1 is Element of K10(K10((D . X1)))

Intersect sf1 is Element of K10((D . X1))

Fi is non empty set

{ b

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

(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