:: CLOSURE2 semantic presentation

K149() is Element of bool K145()

K145() is set

bool K145() is non empty set

K137() is set

bool K137() is non empty set

bool K149() is non empty set

1 is non empty set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() 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

S is set

S is set

S is non empty set

id S is non empty Relation-like S -defined S -valued Function-like one-to-one V17(S) quasi_total Element of bool [:S,S:]

[:S,S:] is non empty Relation-like set

bool [:S,S:] is non empty set

D is Element of S

M is Element of S

(id S) . D is Element of S

(id S) . M is Element of S

S is non empty set

D is non empty Relation-like S -defined Function-like V17(S) set

bool D is non empty Relation-like S -defined Function-like V17(S) additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool D

bool D is non empty Relation-like S -defined Function-like V17(S) set

rng (bool D) is non empty set

union (rng (bool D)) is set

M is non empty Relation-like S -defined Function-like V17(S) ManySortedSubset of D

rng M is non empty set

F is set

d is set

M . d is set

dom (bool D) is non empty set

D . d is set

bool (D . d) is non empty Element of bool (bool (D . d))

bool (D . d) is non empty set

bool (bool (D . d)) is non empty set

(bool D) . d is set

S is set

D is Relation-like S -defined Function-like V17(S) set

bool D is Relation-like S -defined Function-like V17(S) additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

rng (bool D) is set

union (rng (bool D)) is set

Funcs (S,(union (rng (bool D)))) is functional set

M is set

F is set

d is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

dom d is set

rng d is set

[[0]] {} is empty Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional V17( {} ) Function-yielding V25() finite finite-yielding V45() set

{} --> {} is empty Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional V17( {} ) quasi_total Function-yielding V25() finite finite-yielding V45() Element of bool [:{},{{}}:]

{{}} is non empty functional finite V45() set

[:{},{{}}:] is Relation-like finite set

bool [:{},{{}}:] is non empty finite V45() set

{([[0]] {})} is non empty functional finite V45() set

M is set

F is empty Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional V17( {} ) Function-yielding V25() finite finite-yielding V45() set

d is empty Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional V17( {} ) Function-yielding V25() finite finite-yielding V45() ManySortedSubset of F

F is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is set

M is set

M is Relation-like Function-like set

F is Relation-like Function-like set

dom M is set

dom F is set

S is set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is non empty functional Element of bool (S,D)

F is Relation-like Function-like Element of M

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

F is functional Element of bool (S,D)

M \/ F is functional Element of bool (S,D)

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

F is functional Element of bool (S,D)

M /\ F is functional Element of bool (S,D)

S is set

M is Relation-like S -defined Function-like V17(S) set

(S,M) is non empty functional with_common_domain set

bool (S,M) is non empty set

F is functional Element of bool (S,M)

D is set

F \ D is functional Element of bool (S,M)

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

F is functional Element of bool (S,D)

M \+\ F is functional Element of bool (S,D)

M \ F is set

F \ M is set

(M \ F) \/ (F \ M) is set

S is set

D is Relation-like S -defined Function-like V17(S) set

{D} is non empty functional finite set

M is Relation-like S -defined Function-like V17(S) set

(S,M) is non empty functional with_common_domain set

bool (S,M) is non empty set

(S,M) is non empty functional with_common_domain Element of bool (S,M)

S is set

D is Relation-like S -defined Function-like V17(S) set

M is Relation-like S -defined Function-like V17(S) set

(S,M) is non empty functional with_common_domain set

bool (S,M) is non empty set

F is Relation-like S -defined Function-like V17(S) set

{D,F} is non empty functional finite set

{D} is non empty functional finite set

{F} is non empty functional finite set

{D} \/ {F} is non empty finite set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

M /\ F is Relation-like S -defined Function-like V17(S) set

D /\ D is Relation-like S -defined Function-like V17(S) set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

M \/ F is Relation-like S -defined Function-like V17(S) set

D \/ D is Relation-like S -defined Function-like V17(S) set

S is set

D is Relation-like S -defined Function-like V17(S) set

M is Relation-like S -defined Function-like V17(S) set

(S,M) is non empty functional with_common_domain Element of bool (S,M)

(S,M) is non empty functional with_common_domain set

bool (S,M) is non empty set

F is Relation-like S -defined Function-like V17(S) (S,M,(S,M))

F \ D is Relation-like S -defined Function-like V17(S) set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

M \+\ F is Relation-like S -defined Function-like V17(S) set

M \ F is Relation-like S -defined Function-like V17(S) set

F \ M is Relation-like S -defined Function-like V17(S) set

(M \ F) \/ (F \ M) is Relation-like S -defined Function-like V17(S) set

S is functional set

D is non empty functional set

{ (b

{ (dom b

meet { (dom b

M is Relation-like Function-like set

dom M is set

F is set

M . F is set

{ (b

D is Relation-like Function-like set

dom D is set

M is Relation-like Function-like set

dom M is set

F is non empty functional set

{ (dom b

meet { (dom b

F is non empty functional set

{ (dom b

meet { (dom b

d is set

D . d is set

{ (b

M . d is set

f is non empty functional set

{ (dom b

meet { (dom b

d is non empty functional set

{ (dom b

meet { (dom b

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is non empty functional Element of bool (S,D)

(M) is Relation-like Function-like set

dom (M) is set

F is non empty functional set

{ (dom b

meet { (dom b

{S} is non empty finite set

d is set

f is Relation-like Function-like Element of F

dom f is set

the Relation-like Function-like Element of F is Relation-like Function-like Element of F

f is set

dom the Relation-like Function-like Element of F is set

S 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 Relation-like Function-like set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

(M) is Relation-like Function-like set

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]

{{}} is non empty functional finite V45() set

[:S,{{}}:] is Relation-like set

bool [:S,{{}}:] is non empty set

dom (M) is set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V25() finite finite-yielding V45() Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) set

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]

[:S,{{}}:] is Relation-like set

bool [:S,{{}}:] is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

M is functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) set

dom (S,D,M) is set

(M) is Relation-like Function-like set

dom (M) is set

F is non empty functional set

{ (dom b

meet { (dom b

d is set

(S,D,M) . d is set

{ (b

{ (b

x is set

SF is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

SF . d is set

x is set

SF is Relation-like Function-like Element of F

SF . d is set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is non empty functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) set

F is set

(S,D,M) . F is set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

{ (b

d is set

f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

f . F is set

S is Relation-like Function-like set

{S} is non empty functional finite set

({S}) is Relation-like Function-like set

dom ({S}) is set

dom S is set

D is non empty functional set

{ (dom b

meet { (dom b

{(dom S)} is non empty finite set

F is set

d is Relation-like Function-like Element of D

dom d is set

F is set

S is Relation-like Function-like set

dom S is set

D is Relation-like Function-like set

{S,D} is non empty functional finite set

({S,D}) is Relation-like Function-like set

dom ({S,D}) is set

dom D is set

(dom S) /\ (dom D) is set

M is non empty functional set

{ (dom b

meet { (dom b

{(dom S),(dom D)} is non empty finite set

d is set

f is Relation-like Function-like Element of M

dom f is set

d is set

S is set

D is Relation-like Function-like set

dom D is set

{D} is non empty functional finite set

({D}) is Relation-like Function-like set

({D}) . S is set

D . S is set

{(D . S)} is non empty finite set

dom ({D}) is set

M is non empty functional set

{ (dom b

meet { (dom b

{ (b

F is set

d is Relation-like Function-like Element of M

d . S is set

F is set

S is set

D is set

M is Relation-like D -defined Function-like V17(D) set

(D,M) is non empty functional with_common_domain set

bool (D,M) is non empty set

F is Relation-like Function-like set

{F} is non empty functional finite set

F . S is set

{(F . S)} is non empty finite set

d is functional Element of bool (D,M)

(D,M,d) is Relation-like D -defined Function-like V17(D) set

(D,M,d) . S is set

(d) is Relation-like Function-like set

dom (D,M,d) is set

dom F is set

S is set

D is Relation-like Function-like set

D . S is set

M is Relation-like Function-like set

{D,M} is non empty functional finite set

({D,M}) is Relation-like Function-like set

dom ({D,M}) is set

({D,M}) . S is set

M . S is set

{(D . S),(M . S)} is non empty finite set

F is non empty functional set

{ (dom b

meet { (dom b

{ (b

d is set

f is Relation-like Function-like Element of F

f . S is set

d is set

S is set

D is set

M is Relation-like D -defined Function-like V17(D) set

(D,M) is non empty functional with_common_domain set

bool (D,M) is non empty set

F is Relation-like Function-like set

F . S is set

d is Relation-like Function-like set

{F,d} is non empty functional finite set

d . S is set

{(F . S),(d . S)} is non empty finite set

f is functional Element of bool (D,M)

(D,M,f) is Relation-like D -defined Function-like V17(D) set

(D,M,f) . S is set

dom (D,M,f) is set

(f) is Relation-like Function-like set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) set

bool D is Relation-like S -defined Function-like V17(S) set

bool D is Relation-like S -defined Function-like V17(S) additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool D

F is set

(S,D,M) . F is set

(bool D) . F is set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

{ (b

d is set

f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

f . F is set

D . F is set

bool (D . F) is non empty Element of bool (bool (D . F))

bool (D . F) is non empty set

bool (bool (D . F)) is non empty set

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]

[:S,{{}}:] is Relation-like set

bool [:S,{{}}:] is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is Relation-like S -defined Function-like V17(S) set

F is functional Element of bool (S,D)

(S,D,F) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

d is set

M . d is set

(S,D,F) . d is set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

{ (b

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is Relation-like S -defined Function-like V17(S) set

F is Relation-like S -defined Function-like V17(S) set

{M,F} is non empty functional finite set

M \/ F is Relation-like S -defined Function-like V17(S) set

d is functional Element of bool (S,D)

(S,D,d) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

union (S,D,d) is Relation-like S -defined Function-like V17(S) set

f is set

(union (S,D,d)) . f is set

(S,D,d) . f is set

union ((S,D,d) . f) is set

M . f is set

F . f is set

{(M . f),(F . f)} is non empty finite set

union {(M . f),(F . f)} is set

(M . f) \/ (F . f) is set

(M \/ F) . f is set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

M is functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

{F,d} is non empty functional finite set

F /\ d is Relation-like S -defined Function-like V17(S) set

q is set

D . q is set

bool (D . q) is non empty set

bool (bool (D . q)) is non empty set

f is non empty functional Element of bool (S,D)

(S,D,f) is Relation-like non-empty S -defined Function-like V17(S) ManySortedSubset of bool D

(S,D,f) . q is set

meet (S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

(meet (S,D,f)) . q is set

(meet (S,D,M)) . q is set

meet ((S,D,f) . q) is set

F . q is set

d . q is set

{(F . q),(d . q)} is non empty finite set

meet {(F . q),(d . q)} is set

(F . q) /\ (d . q) is set

(F /\ d) . q is set

x is Element of bool (bool (D . q))

Intersect x is Element of bool (D . q)

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

F is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

d is set

F . d is set

(meet (S,D,M)) . d is set

D . d is set

bool (D . d) is non empty set

bool (bool (D . d)) is non empty set

(S,D,M) . d is set

f is Element of bool (bool (D . d))

Intersect f is Element of bool (D . d)

q is set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

{ (b

x is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

x . d is set

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]

[:S,{{}}:] is Relation-like set

bool [:S,{{}}:] is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

(S,D,(S,D)) is Relation-like non-empty S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

bool D is Relation-like S -defined Function-like V17(S) additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool D

M is set

(S,D,(S,D)) . M is set

{ (b

(bool D) . M is set

F is set

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

d . M is set

D . M is set

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

bool (D . M) is non empty set

bool (bool (D . M)) is non empty set

F is set

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]

[:S,{{}}:] is Relation-like set

bool [:S,{{}}:] is non empty set

M .--> F is Relation-like {M} -defined Function-like one-to-one finite set

{M} is non empty finite set

{M} --> F is non empty Relation-like {M} -defined Function-like constant V17({M}) quasi_total finite Element of bool [:{M},{F}:]

{F} is non empty finite set

[:{M},{F}:] is non empty Relation-like finite set

bool [:{M},{F}:] is non empty finite V45() set

([[0]] S) +* (M .--> F) is Relation-like Function-like set

dom (([[0]] S) +* (M .--> F)) is set

dom (M .--> F) is finite set

d is Relation-like S -defined Function-like V17(S) set

d . M is set

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

f is set

d . f is set

D . f is set

bool (D . f) is non empty Element of bool (bool (D . f))

bool (D . f) is non empty set

bool (bool (D . f)) is non empty set

([[0]] S) . f 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 Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is Relation-like S -defined Function-like V17(S) set

F is Relation-like S -defined Function-like V17(S) set

M \/ F is Relation-like S -defined Function-like V17(S) set

M is functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

union (S,D,M) is Relation-like S -defined Function-like V17(S) set

M is Relation-like S -defined Function-like V17(S) set

F is Relation-like S -defined Function-like V17(S) set

M /\ F is Relation-like S -defined Function-like V17(S) set

M is functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]

[:S,{{}}:] is Relation-like set

bool [:S,{{}}:] is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

F is Relation-like S -defined Function-like V17(S) set

d is Relation-like S -defined Function-like V17(S) set

F \/ d is Relation-like S -defined Function-like V17(S) set

{F,d} is non empty functional finite set

{F} is non empty functional finite set

{d} is non empty functional finite set

{F} \/ {d} is non empty finite set

f is functional Element of bool (S,D)

(S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

union (S,D,f) is Relation-like S -defined Function-like V17(S) set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

F is Relation-like S -defined Function-like V17(S) set

d is Relation-like S -defined Function-like V17(S) set

F /\ d is Relation-like S -defined Function-like V17(S) set

{F,d} is non empty functional finite set

{F} is non empty functional finite set

{d} is non empty functional finite set

{F} \/ {d} is non empty finite set

f is functional Element of bool (S,D)

(S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

meet (S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

F is functional Element of bool (S,D)

M is functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]

[:S,{{}}:] is Relation-like set

bool [:S,{{}}:] is non empty set

meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

F is functional Element of bool (S,D)

M is functional Element of bool (S,D)

(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

bool D is Relation-like S -defined Function-like V17(S) set

[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set

S --> {} is Relation-like S -defined Function-like constant V17(S) quasi_total Function-yielding V25() Element of bool [:S,{{}}:]

[:S,{{}}:] is Relation-like set

bool [:S,{{}}:] is non empty set

union (S,D,M) is Relation-like S -defined Function-like V17(S) set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

M is functional Element of bool (S,D)

S is set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

M . F is set

M . F is Relation-like Function-like Element of (S,D)

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F \/ d is Relation-like S -defined Function-like V17(S) set

M . (F \/ d) is set

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

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

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

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

id (S,D) is non empty Relation-like (S,D) -defined (S,D) -valued Function-like one-to-one V17((S,D)) quasi_total Function-yielding V25() Element of bool [:(S,D),(S,D):]

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F \/ d is Relation-like S -defined Function-like V17(S) set

M . (F \/ d) is set

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

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

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

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

(S,D,F,M) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,M,F)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

M /\ F is Relation-like S -defined Function-like V17(S) set

d is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

(S,D,d,M) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,d,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

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

f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,d,f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

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

F \/ d is Relation-like S -defined Function-like V17(S) set

M . (F \/ d) is set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

F is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

M \ F is Relation-like S -defined Function-like V17(S) set

d is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

(S,D,d,M) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,d,F) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,d,M) \ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set

f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,d,f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

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

M \/ F is Relation-like S -defined Function-like V17(S) set

d . (M \/ F) is set

(M \ F) \/ F is Relation-like S -defined Function-like V17(S) set

d . ((M \ F) \/ F) is set

(S,D,d,f) \/ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set

((S,D,d,f) \/ (S,D,d,F)) \ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set

(S,D,d,f) \ (S,D,d,F) is Relation-like S -defined Function-like V17(S) set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

M * F is Relation-like Function-like set

F * M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

(S,D,F,M) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,(S,D,F,M),d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,F,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

dom F is non empty set

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

(S,D,F,M) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]

dom F is non empty set

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,(S,D,F,M),d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,(S,D,F,M),f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,F,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,F,f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,f)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

(S,D,F,M) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]

(S,D,M,F) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,(S,D,F,M),d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,(S,D,F,M),(S,D,(S,D,F,M),d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

dom M is non empty set

dom F is non empty set

(S,D,F,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,F,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,(S,D,F,d))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,M,(S,D,F,(S,D,F,d)))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,(S,D,M,F),(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,(S,D,M,F),(S,D,F,d))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,F,(S,D,M,(S,D,F,d))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,(S,D,M,(S,D,F,d)))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,F,(S,D,(S,D,F,M),d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,(S,D,(S,D,F,M),d))) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

S is set

D is Relation-like S -defined Function-like V17(S) set

(S,D) is non empty functional with_common_domain (S,D) (S,D) (S,D) (S,D) (S,D) (S,D) Element of bool (S,D)

(S,D) is non empty functional with_common_domain set

bool (S,D) is non empty set

[:(S,D),(S,D):] is non empty Relation-like set

bool [:(S,D),(S,D):] is non empty set

M is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

F is non empty Relation-like Function-like V17((S,D)) quasi_total Element of bool [:(S,D),(S,D):]

(S,D,F,M) is non empty Relation-like Function-like V17((S,D)) quasi_total quasi_total Element of bool [:(S,D),(S,D):]

d is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

d \/ f is Relation-like S -defined Function-like V17(S) set

(S,D,F,M) . (d \/ f) is set

(S,D,(S,D,F,M),d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,(S,D,F,M),f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,(S,D,F,M),d) \/ (S,D,(S,D,F,M),f) is Relation-like S -defined Function-like V17(S) set

dom F is non empty set

F . (d \/ f) is set

M . (F . (d \/ f)) is set

(S,D,F,d) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,F,f) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,F,d) \/ (S,D,F,f) is Relation-like S -defined Function-like V17(S) set

M . ((S,D,F,d) \/ (S,D,F,f)) is set

(S,D,M,(S,D,F,d)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,f)) is Relation-like S -defined Function-like V17(S) (S,D,(S,D))

(S,D,M,(S,D,F,d)) \/ (S,D,M,(S,D,F,f)) is Relation-like S -defined Function-like V17(S) set

(S,D,(S,D,F,M),d) \/ (S,D,M,(S,D,F,f)) is Relation-like S -defined Function-like V17(S) 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 V17( the carrier of S) set

the carrier of S is set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

(S, the Sorts of D,( the carrier of S, 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 V17( the carrier of S) set

the carrier of S is set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

(S, the Sorts of D,( the carrier of S, the Sorts of D)) is (S) (S)

the Sorts of (S,D) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the of (S,D) is functional Element of bool ( the carrier of S, the Sorts of (S,D))

( the carrier of S, the Sorts of (S,D)) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of (S,D)) is non empty 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 V17( the carrier of S) set

the carrier of S is set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

(S, the Sorts of D,( the carrier of S, 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 V17( the carrier of S) set

the carrier of S is set

( the carrier of S, the Sorts of the non-empty many-sorted over S) is non empty functional with_common_domain ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) ( the carrier of S, the Sorts of the non-empty many-sorted over S) Element of bool ( the carrier of S, the Sorts of the non-empty many-sorted over S)

( the carrier of S, the Sorts of the non-empty many-sorted over S) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of the non-empty many-sorted over S) is non empty set

(S, the Sorts of the non-empty many-sorted over S,( the carrier of S, 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

S is 1-sorted

the carrier of S is set

D is Relation-like non-empty the carrier of S -defined Function-like V17( the carrier of S) set

( the carrier of S,D) is non empty functional with_common_domain set

bool ( the carrier of S,D) is non empty set

M is functional Element of bool ( 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 V17( the carrier of S) 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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

M is functional ( the carrier of S, the Sorts of D) Element of bool ( 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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

M is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( 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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

M is functional ( the carrier of S, the Sorts of D) Element of bool ( 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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

M is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( 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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

M is non empty functional ( the carrier of S, the Sorts of D) Element of bool ( 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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

M is non empty functional ( the carrier of S, the Sorts of D) Element of bool ( 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty 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 V17( the carrier of S) set

the of D is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

S is set

S is 1-sorted

the carrier of S is set

D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

( the carrier of S,D) is non empty functional with_common_domain ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool ( the carrier of S,D)

( the carrier of S,D) is non empty functional with_common_domain set

bool ( the carrier of S,D) is non empty set

[:( the carrier of S,D),( the carrier of S,D):] is non empty Relation-like set

bool [:( the carrier of S,D),( the carrier of S,D):] is non empty set

M is non empty Relation-like Function-like V17(( the carrier of S,D)) quasi_total ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool [:( the carrier of S,D),( the carrier of S,D):]

{ b

{ b

bool ( the carrier of S,D) is non empty set

d is functional Element of bool ( the carrier of S,D)

(S,D,d) is (S) (S)

the Sorts of (S,D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the of (S,D,d) is functional Element of bool ( the carrier of S, the Sorts of (S,D,d))

( the carrier of S, the Sorts of (S,D,d)) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of (S,D,d)) is non empty set

F is (S) (S)

the Sorts of F is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the of F is functional Element of bool ( the carrier of S, the Sorts of F)

( the carrier of S, the Sorts of F) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of F) is non empty set

d is (S) (S)

the Sorts of d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the of d is functional Element of bool ( the carrier of S, the Sorts of d)

( the carrier of S, the Sorts of d) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of d) is non empty set

S is 1-sorted

the carrier of S is set

D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

( the carrier of S,D) is non empty functional with_common_domain ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool ( the carrier of S,D)

( the carrier of S,D) is non empty functional with_common_domain set

bool ( the carrier of S,D) is non empty set

[:( the carrier of S,D),( the carrier of S,D):] is non empty Relation-like set

bool [:( the carrier of S,D),( the carrier of S,D):] is non empty set

M is non empty Relation-like Function-like V17(( the carrier of S,D)) quasi_total ( the carrier of S,D) ( the carrier of S,D) ( the carrier of S,D) Element of bool [:( the carrier of S,D),( 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 V17( the carrier of S) set

{ b

the of (S,D,M) is functional Element of bool ( the carrier of S, the Sorts of (S,D,M))

( the carrier of S, the Sorts of (S,D,M)) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of (S,D,M)) is non empty set

bool ( the carrier of S,D) is non empty set

d is functional Element of bool ( the carrier of S,D)

(S,D,d) is (S) (S)

f is functional Element of bool ( the carrier of S,D)

( the carrier of S,D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool D

bool D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

meet ( the carrier of S,D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of D

x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))

SF is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))

( the carrier of S,D,M,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))

SF9 is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))

( the carrier of S,D,M,SF9) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S,D,( the carrier of S,D))

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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

M is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D

the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

{ b

{ b

bool ( the carrier of S, the Sorts of D) is non empty set

F is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D,F) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D

bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

meet ( the carrier of S, the Sorts of D,F) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D

d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

F is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

f is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D

bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

meet ( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D

d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

q is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D

meet ( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D

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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

[:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty Relation-like set

bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty set

the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

M is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

F is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]

( the carrier of S, the Sorts of D,F,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

(S,D,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

{ b

d is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D

bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

meet ( the carrier of S, the Sorts of D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D

f is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

[:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty Relation-like set

bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty set

the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

M is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

F is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]

( the carrier of S, the Sorts of D,F,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

{ H

q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

{ H

{ H

(S,D,M) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

{ b

q is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D

bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

meet ( the carrier of S, the Sorts of D,q) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D

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 V17( the carrier of S) set

( the carrier of S, the Sorts of D) is non empty functional with_common_domain ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D) is non empty functional with_common_domain set

bool ( the carrier of S, the Sorts of D) is non empty set

[:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty Relation-like set

bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):] is non empty set

M is non empty Relation-like Function-like V17(( the carrier of S, the Sorts of D)) quasi_total Element of bool [:( the carrier of S, the Sorts of D),( the carrier of S, the Sorts of D):]

d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

( the carrier of S, the Sorts of D,M,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

(S,D,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

the of D is non empty functional ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) ( the carrier of S, the Sorts of D) Element of bool ( the carrier of S, the Sorts of D)

{ b

f is functional Element of bool ( the carrier of S, the Sorts of D)

( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of D

bool the Sorts of D is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

meet ( the carrier of S, the Sorts of D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of D

q is Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

x is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

d is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

f is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

( the carrier of S, the Sorts of D,M,d) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

( the carrier of S, the Sorts of D,M,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

(S,D,f) is Relation-like the carrier of S -defined Function-like V17( the carrier of S) ( the carrier of S, the Sorts of D,( the carrier of S, the Sorts of D))

the of D is non empty functional ( the carrier of S, the Sorts of D) ( the