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

S is set
S is set
S is non empty set

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

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

dom d is set
rng d is set

is non empty functional finite V45() set

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

S is set

(S,D) is set
M is set

dom M is set
dom F is set
S is set
S is set

(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
S is 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

(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,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 is 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

(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

(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

(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 non empty functional finite 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

(S,M) is non empty functional with_common_domain set
bool (S,M) is non empty 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

(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))

S is 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))

S is 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))

S is 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) \/ (F \ M) is Relation-like S -defined Function-like V17(S) set

D is non empty functional set
{ (b1 . a1) where b1 is Relation-like Function-like Element of D : verum } is set
{ (dom b1) where b1 is Relation-like Function-like Element of D : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of D : verum } is set

dom M is set
F is set
M . F is set
{ (b1 . F) where b1 is Relation-like Function-like Element of D : verum } is set

dom D is set

dom M is set
F is non empty functional set
{ (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
F is non empty functional set
{ (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
d is set
D . d is set
{ (b1 . d) where b1 is Relation-like Function-like Element of F : verum } is set
M . d is set
f is non empty functional set
{ (dom b1) where b1 is Relation-like Function-like Element of f : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of f : verum } is set
d is non empty functional set
{ (dom b1) where b1 is Relation-like Function-like Element of d : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of d : verum } is set
S is 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)

dom (M) is set
F is non empty functional set
{ (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
{S} is non empty finite set
d is set

dom f is set

f is set

S is 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)

is non empty functional finite V45() set

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

(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set

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

bool [:S,:] is non empty set
S is 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

dom (M) is set
F is non empty functional set
{ (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
d is set
(S,D,M) . d is set
{ (b1 . d) where b1 is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b1 in M } is set
{ (b1 . d) where b1 is Relation-like Function-like Element of F : verum } is set
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 . d is set
S is 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)
{ (b1 . F) where b1 is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b1 in M } is set
d is set
f is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
f . F is set

{S} is non empty functional finite set

dom ({S}) is set
dom S is set
D is non empty functional set
{ (dom b1) where b1 is Relation-like Function-like Element of D : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of D : verum } is set
{(dom S)} is non empty finite set
F is set

dom d is set
F is set

dom S is 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 b1) where b1 is Relation-like Function-like Element of M : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of M : verum } is set
{(dom S),(dom D)} is non empty finite set
d is set

dom f is set
d is set
S is set

dom D is set
{D} is non empty functional finite 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 b1) where b1 is Relation-like Function-like Element of M : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of M : verum } is set
{ (b1 . S) where b1 is Relation-like Function-like Element of M : verum } is set
F is set

d . S is set
F is set
S is set
D is set

(D,M) is non empty functional with_common_domain set
bool (D,M) is non empty 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

dom (D,M,d) is set
dom F is set
S is set

D . S is 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 b1) where b1 is Relation-like Function-like Element of F : verum } is set
meet { (dom b1) where b1 is Relation-like Function-like Element of F : verum } is set
{ (b1 . S) where b1 is Relation-like Function-like Element of F : verum } is set
d is set

f . S is set
d is set
S is set
D is set

(D,M) is non empty functional with_common_domain set
bool (D,M) is non empty set

F . S is 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

S is 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

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)
{ (b1 . F) where b1 is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b1 in M } is set
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

bool [:S,:] is non empty set
S is 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)
(S,D,F) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

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)
{ (b1 . d) where b1 is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b1 in F } is set
S is set

(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set

{M,F} is non empty functional finite 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

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

(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

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

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

(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

meet (S,D,M) 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)
{ (b1 . d) where b1 is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b1 in M } is set
x is Relation-like S -defined Function-like V17(S) (S,D,(S,D))
x . d is set

bool [:S,:] is non empty set
S is 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

M is set
(S,D,(S,D)) . M is set
{ (b1 . M) where b1 is Relation-like S -defined Function-like V17(S) (S,D,(S,D)) : b1 in (S,D) } is set
(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

bool [:S,:] is non empty set

{M} is non empty finite set

{F} is non empty finite set
[:{M},{F}:] is non empty Relation-like finite set
bool [:{M},{F}:] is non empty finite V45() set
() +* (M .--> F) is Relation-like Function-like set
dom (() +* (M .--> F)) is set
dom (M .--> F) is finite 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

S is set

(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
S is 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 functional Element of bool (S,D)
(S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool D

union (S,D,M) 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

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

bool [:S,:] is non empty set
S is 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

(S,D) is non empty functional with_common_domain set
bool (S,D) is non empty set
S is 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,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

union (S,D,f) is Relation-like S -defined Function-like V17(S) set
S is 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,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

meet (S,D,f) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
S is 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 [:S,:] is non empty set
meet (S,D,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of D
S is 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,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 [:S,:] is non empty set
union (S,D,M) is Relation-like S -defined Function-like V17(S) set
S is 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

(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

(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

(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))

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

(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

(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

(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

(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))

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

(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

(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

(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))

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

(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

M . (F \/ d) is set
S is 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))

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

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

(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):]

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

(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

(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

(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))

(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):]
{ b1 where b1 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,b1) = b1 } is set
{ b1 where b1 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)) : S1[b1] } is 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)
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
{ b1 where b1 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)) : S1[b1] } is set
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)
{ b1 where b1 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)) : ( M c= b1 & b1 in the of D ) } is set
{ b1 where b1 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)) : S1[b1] } is set
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))
{ b1 where b1 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)) : ( M c= b1 & b1 in the of D ) } is set
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))
{ H1(b1) where b1 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)) : ( H1(b1) in the of D & S1[b1] ) } is 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))
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))
{ H1(b1) where b1 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)) : S2[b1] } is set
{ H1(b1) where b1 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)) : S3[b1] } is set
(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))
{ b1 where b1 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)) : ( M c= b1 & b1 in the of D ) } is set
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)
{ b1 where b1 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 c= b1 & b1 in the of D ) } is 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
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