:: VALUED_0 semantic presentation

REAL is complex-membered ext-real-membered real-membered V21() set

NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Element of bool REAL

bool REAL is non empty set

{} is complex empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V40() ext-real set

the complex empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V40() ext-real set is complex empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V40() ext-real set

COMPLEX is complex-membered V21() set

RAT is complex-membered ext-real-membered real-membered rational-membered V21() set

INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V21() set

ExtREAL is ext-real-membered set

dom {} is complex empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V40() ext-real set

rng {} is complex empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V40() ext-real with_non-empty_elements set

omega is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() set

0 is complex empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V40() ext-real Element of NAT

1 is complex non empty epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real positive Element of NAT

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

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

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like () set

rng X is set

X is Relation-like () set

rng X is set

X is Relation-like () () () set

rng X is complex-membered ext-real-membered set

X is Relation-like RAT -valued () () () set

rng X is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT

bool RAT is non empty set

X is Relation-like INT -valued () () () set

rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool INT

bool INT is non empty set

X is Relation-like RAT -valued () () () () set

rng X is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT

X is Relation-like set

c

rng X is set

rng c

X is Relation-like set

c

rng X is set

rng c

X is Relation-like set

c

rng X is set

rng c

X is Relation-like set

c

X is Relation-like set

c

X is Relation-like set

c

rng X is set

rng c

X is Relation-like () set

bool X is non empty set

c

X is Relation-like () set

bool X is non empty set

c

X is Relation-like () () () set

bool X is non empty set

c

X is Relation-like RAT -valued () () () set

bool X is non empty set

c

X is Relation-like INT -valued () () () set

bool X is non empty set

c

X is Relation-like RAT -valued () () () () set

bool X is non empty set

c

X is Relation-like () set

c

X \/ c

rng (X \/ c

rng X is complex-membered set

rng c

(rng X) \/ (rng c

X is Relation-like () set

c

X \/ c

rng (X \/ c

rng X is ext-real-membered set

rng c

(rng X) \/ (rng c

X is Relation-like () () () set

c

X \/ c

rng (X \/ c

rng X is complex-membered ext-real-membered real-membered set

rng c

(rng X) \/ (rng c

X is Relation-like RAT -valued () () () set

c

X \/ c

X is Relation-like INT -valued () () () set

c

X \/ c

X is Relation-like RAT -valued () () () () set

c

X \/ c

rng (X \/ c

rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT

rng c

(rng X) \/ (rng c

X is Relation-like () set

c

X /\ c

rng (X /\ c

rng X is complex-membered set

X \ c

bool X is non empty set

X is Relation-like () set

c

X /\ c

rng (X /\ c

rng X is ext-real-membered set

X \ c

bool X is non empty set

X is Relation-like () () () set

c

X /\ c

rng (X /\ c

rng X is complex-membered ext-real-membered real-membered set

X \ c

bool X is non empty set

X is Relation-like RAT -valued () () () set

c

X /\ c

X \ c

bool X is non empty set

X is Relation-like INT -valued () () () set

c

X /\ c

X \ c

bool X is non empty set

X is Relation-like RAT -valued () () () () set

c

X /\ c

rng (X /\ c

rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT

X \ c

bool X is non empty set

X is Relation-like () set

c

X \+\ c

X \ c

c

(X \ c

X is Relation-like () set

c

X \+\ c

X \ c

c

(X \ c

X is Relation-like () () () set

c

X \+\ c

X \ c

c

(X \ c

X is Relation-like RAT -valued () () () set

c

X \+\ c

X \ c

c

(X \ c

X is Relation-like INT -valued () () () set

c

X \+\ c

X \ c

c

(X \ c

X is Relation-like RAT -valued () () () () set

c

X \+\ c

X \ c

c

(X \ c

X is Relation-like () set

c

X .: c

rng X is complex-membered set

X is Relation-like () set

c

X .: c

rng X is ext-real-membered set

X is Relation-like () () () set

c

X .: c

rng X is complex-membered ext-real-membered real-membered set

X is Relation-like RAT -valued () () () set

c

X .: c

rng X is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT

X is Relation-like INT -valued () () () set

c

X .: c

rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool INT

X is Relation-like RAT -valued () () () () set

c

X .: c

rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT

X is Relation-like () set

c

Im (X,c

{c

X .: {c

X is Relation-like () set

c

Im (X,c

{c

X .: {c

X is Relation-like () () () set

c

Im (X,c

{c

X .: {c

X is Relation-like RAT -valued () () () set

c

Im (X,c

{c

X .: {c

X is Relation-like INT -valued () () () set

c

Im (X,c

{c

X .: {c

X is Relation-like RAT -valued () () () () set

c

Im (X,c

{c

X .: {c

X is Relation-like () set

c

X | c

rng X is complex-membered set

rng (X | c

X is Relation-like () set

c

X | c

rng X is ext-real-membered set

rng (X | c

X is Relation-like () () () set

c

X | c

rng X is complex-membered ext-real-membered real-membered set

rng (X | c

X is Relation-like RAT -valued () () () set

c

X | c

X is Relation-like INT -valued () () () set

c

X | c

X is Relation-like RAT -valued () () () () set

c

X | c

rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT

rng (X | c

X is complex-membered set

id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total Element of bool [:X,X:]

[:X,X:] is Relation-like set

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

rng (id X) is complex-membered Element of bool X

bool X is non empty set

X is ext-real-membered set

id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total Element of bool [:X,X:]

[:X,X:] is Relation-like set

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

rng (id X) is ext-real-membered Element of bool X

bool X is non empty set

X is complex-membered ext-real-membered real-membered set

id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total () () Element of bool [:X,X:]

[:X,X:] is Relation-like set

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

rng (id X) is complex-membered ext-real-membered real-membered Element of bool X

bool X is non empty set

X is complex-membered ext-real-membered real-membered rational-membered set

id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total () () () Element of bool [:X,X:]

[:X,X:] is Relation-like set

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

rng (id X) is complex-membered ext-real-membered real-membered rational-membered Element of bool X

bool X is non empty set

X is complex-membered ext-real-membered real-membered rational-membered integer-membered set

id X is Relation-like X -defined X -valued RAT -valued Function-like one-to-one total quasi_total () () () Element of bool [:X,X:]

[:X,X:] is Relation-like set

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

rng (id X) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool X

bool X is non empty set

X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

id X is Relation-like X -defined X -valued RAT -valued INT -valued Function-like one-to-one total quasi_total () () () Element of bool [:X,X:]

[:X,X:] is Relation-like set

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

rng (id X) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool X

bool X is non empty set

X is Relation-like set

c

X * c

rng c

rng (X * c

X is Relation-like set

c

X * c

rng c

rng (X * c

X is Relation-like set

c

X * c

rng c

rng (X * c

X is Relation-like set

c

X * c

X is Relation-like set

c

X * c

X is Relation-like set

c

X * c

rng c

rng (X * c

X is Relation-like Function-like set

dom X is set

c

X . c

n1 is Relation-like Function-like () set

n1 . c

rng n1 is complex-membered set

c

rng X is set

n1 is set

X . n1 is set

c

X . c

n1 is Relation-like Function-like () set

n1 . c

rng n1 is ext-real-membered set

c

rng X is set

n1 is set

X . n1 is set

c

X . c

n1 is Relation-like Function-like () () () set

n1 . c

rng n1 is complex-membered ext-real-membered real-membered set

c

rng X is set

n1 is set

X . n1 is set

c

X . c

n1 is Relation-like RAT -valued Function-like () () () () set

n1 . c

rng n1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT

c

rng X is set

n1 is set

X . n1 is set

X is Relation-like Function-like set

c

dom X is set

X . c

c

dom X is set

X . c

c

dom X is set

dom X is set

c

X . c

X is Relation-like Function-like set

c

dom X is set

X . c

c

dom X is set

X . c

c

dom X is set

dom X is set

c

X . c

X is Relation-like Function-like set

c

dom X is set

X . c

c

dom X is set

X . c

c

dom X is set

dom X is set

c

X . c

X is Relation-like Function-like set

c

dom X is set

X . c

rng X is set

c

dom X is set

X . c

c

dom X is set

c

rng X is set

dom X is set

n1 is set

X . n1 is set

X is Relation-like Function-like set

c

dom X is set

X . c

rng X is set

c

dom X is set

X . c

c

dom X is set

c

rng X is set

dom X is set

n1 is set

X . n1 is set

X is Relation-like Function-like set

c

dom X is set

X . c

c

dom X is set

X . c

c

dom X is set

dom X is set

c

X . c

X is Relation-like Function-like () set

c

X . c

X is Relation-like Function-like () set

c

X . c

X is Relation-like Function-like () () () set

c

X . c

X is Relation-like RAT -valued Function-like () () () set

c

X . c

X is Relation-like INT -valued Function-like () () () set

c

X . c

X is Relation-like RAT -valued Function-like () () () () set

c

X . c

X is set

c

X --> c

{c

[:X,{c

bool [:X,{c

rng (X --> c

bool {c

X is set

c

X --> c

{c

[:X,{c

bool [:X,{c

rng (X --> c

bool {c

X is set

c

X --> c

{c

[:X,{c

bool [:X,{c

rng (X --> c

bool {c

X is set

c

X --> c

{c

[:X,{c

bool [:X,{c

rng (X --> c

bool {c

X is set

c

X --> c

{c

[:X,{c

bool [:X,{c

rng (X --> c

bool {c

X is set

c

X --> c

{c

[:X,{c

bool [:X,{c

rng (X --> c

bool {c

X is Relation-like Function-like () set

c

X +* c

rng (X +* c

rng X is complex-membered set

rng c

(rng X) \/ (rng c

X is Relation-like Function-like () set

c

X +* c

rng (X +* c

rng X is ext-real-membered set

rng c

(rng X) \/ (rng c

X is Relation-like Function-like () () () set

c

X +* c

rng (X +* c

rng X is complex-membered ext-real-membered real-membered set

rng c

(rng X) \/ (rng c

X is Relation-like RAT -valued Function-like () () () set

c

X +* c

rng (X +* c

rng X is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT

rng c

(rng X) \/ (rng c

X is Relation-like INT -valued Function-like () () () set

c

X +* c

rng (X +* c

rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool INT

rng c

(rng X) \/ (rng c

X is Relation-like RAT -valued Function-like () () () () set

c

X +* c

rng (X +* c

rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT

rng c

(rng X) \/ (rng c

X is set

c

X .--> c

{X} is non empty trivial set

{X} --> c

{c

[:{X},{c

bool [:{X},{c

X is set

c

X .--> c

{X} is non empty trivial set

{X} --> c

{c

[:{X},{c

bool [:{X},{c

X is set

c

X .--> c

{X} is non empty trivial set

{X} --> c

{c

[:{X},{c

bool [:{X},{c

X is set

c

X .--> c

{X} is non empty trivial set

{X} --> c

{c

[:{X},{c

bool [:{X},{c

X is set

c

X .--> c

{X} is non empty trivial set

{X} --> c

{c

[:{X},{c

bool [:{X},{c

X is set

c

X .--> c

{X} is non empty trivial set

{X} --> c

{c

[:{X},{c

bool [:{X},{c

X is set

c

[:X,c

bool [:X,c

n1 is Relation-like X -defined c

rng n1 is complex-membered Element of bool c

bool c

X is set

c

[:X,c

bool [:X,c

n1 is Relation-like X -defined c

rng n1 is ext-real-membered Element of bool c

bool c

X is set

c

[:X,c

bool [:X,c

n1 is Relation-like X -defined c

rng n1 is complex-membered ext-real-membered real-membered Element of bool c

bool c

X is set

c

[:X,c

bool [:X,c

n1 is Relation-like X -defined c

rng n1 is complex-membered ext-real-membered real-membered rational-membered Element of bool c

bool c

X is set

c

[:X,c

bool [:X,c

n1 is Relation-like X -defined c

rng n1 is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool c

bool c

X is set

c

[:X,c

bool [:X,c

n1 is Relation-like X -defined c

rng n1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool c

bool c

X is set

c

[:X,c

rng [:X,c

X is set

c

[:X,c

rng [:X,c

X is set

c

[:X,c

rng [:X,c

X is set

c

[:X,c

rng [:X,c

X is set

c

[:X,c

rng [:X,c

X is set

c

[:X,c

rng [:X,c

1 .--> 1 is Relation-like NAT -defined {1} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one () () () () set

{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered with_non-empty_elements non empty-membered set

{1} --> 1 is non empty Relation-like non-empty non empty-yielding {1} -defined NAT -valued RAT -valued INT -valued {1} -valued Function-like constant total quasi_total () () () () Element of bool [:{1},{1}:]

[:{1},{1}:] is non empty Relation-like RAT -valued INT -valued () () () () set

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

X is non empty Relation-like Function-like constant () set

dom X is non empty set

c

n1 is set

X . n1 is complex set

X is non empty Relation-like Function-like constant () set

dom X is non empty set

c

n1 is set

X . n1 is ext-real set

X is non empty Relation-like Function-like constant () () () set

dom X is non empty set

c

n1 is set

X . n1 is complex real ext-real set

X is non empty Relation-like RAT -valued Function-like constant () () () set

dom X is non empty set

c

n1 is set

X . n1 is complex real rational ext-real set

X is non empty Relation-like INT -valued Function-like constant () () () set

dom X is non empty set

c

n1 is set

X . n1 is complex real integer rational ext-real set

X is non empty Relation-like RAT -valued Function-like constant () () () () set

dom X is non empty set

c

n1 is set

X . n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

X is Relation-like Function-like () set

c

dom X is set

X . c

n1 is ext-real set

X . n1 is ext-real set

c

dom X is set

X . c

n1 is ext-real set

X . n1 is ext-real set

X is Relation-like Function-like () set

c

dom X is set

X . c

n1 is ext-real set

X . n1 is ext-real set

X is Relation-like Function-like () set

c

dom X is set

X . c

n1 is ext-real set

X . n1 is ext-real set

X is Relation-like Function-like () () () set

c

X * c

n1 is ext-real set

dom (X * c

(X * c

n2 is ext-real set

(X * c

dom X is set

X . n1 is ext-real set

c

X . n2 is ext-real set

c

dom c

X is Relation-like Function-like () () set

c

X * c

n1 is ext-real set

dom (X * c

(X * c

n2 is ext-real set

(X * c

dom X is set

X . n1 is ext-real set

c

X . n2 is ext-real set

c

dom c

X is Relation-like Function-like () () () set

c

X * c

n1 is ext-real set

dom (X * c

(X * c

n2 is ext-real set

(X * c

dom X is set

X . n1 is ext-real set

c

X . n2 is ext-real set

c

dom c

X is Relation-like Function-like () () set

c

X * c

n1 is ext-real set

dom (X * c

(X * c

n2 is ext-real set

(X * c

dom X is set

X . n1 is ext-real set

c

X . n2 is ext-real set

c

dom c

X is Relation-like Function-like () () () set

c

X * c

n1 is ext-real set

dom (X * c

(X * c

n2 is ext-real set

(X * c

dom X is set

X . n1 is ext-real set

c

X . n2 is ext-real set

c

dom c

c

n1 is ext-real set

dom (c

(c

n2 is ext-real set

(c

dom c

c

X . (c

c

X . (c

dom X is set

X is Relation-like Function-like () () set

c

X * c

n1 is ext-real set

dom (X * c

(X * c

n2 is ext-real set

(X * c

dom X is set

X . n1 is ext-real set

c

X . n2 is ext-real set

c

dom c

c

n1 is ext-real set

dom (c

(c

n2 is ext-real set

(c

dom c

c

X . (c

c

X . (c

dom X is set

X is ext-real-membered set

[:X,X:] is Relation-like () set

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

id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total () Element of bool [:X,X:]

c

dom (id X) is set

(id X) . c

n1 is ext-real set

(id X) . n1 is ext-real set

dom (id X) is ext-real-membered Element of bool X

bool X is non empty set

c

id NAT is non empty Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like one-to-one total quasi_total () () () () () () Element of bool [:NAT,NAT:]

X is non empty Relation-like NAT -defined Function-like total set

id NAT is non empty Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like one-to-one total quasi_total () () () () () () Element of bool [:NAT,NAT:]

(id NAT) * X is non empty Relation-like NAT -defined Function-like total set

dom X is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

bool NAT is non empty set

c

rng c

n1 is non empty Relation-like NAT -defined Function-like total (c

rng n1 is non empty set

n2 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]

n2 * c

X is non empty set

c

n1 is non empty Relation-like NAT -defined Function-like total (c

rng n1 is non empty set

rng c

bool X is non empty set

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

n1 is non empty Relation-like NAT -defined X -valued Function-like total (c

rng n1 is non empty Element of bool X

bool X is non empty set

dom n1 is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

bool NAT is non empty set

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

c

id NAT is non empty Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like one-to-one total quasi_total () () () () () () Element of bool [:NAT,NAT:]

(id NAT) ^\ n1 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () Element of bool [:NAT,NAT:]

h1 is ext-real set

dom ((id NAT) ^\ n1) is non empty set

((id NAT) ^\ n1) . h1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

h2 is ext-real set

((id NAT) ^\ n1) . h2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

dom ((id NAT) ^\ n1) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

bool NAT is non empty set

j is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

((id NAT) ^\ n1) . j is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

j + n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

(id NAT) . (j + n1) is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

n is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

((id NAT) ^\ n1) . n is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

n + n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

(id NAT) . (n + n1) is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

c

h1 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]

h1 * c

c

(c

c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

id NAT is non empty Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like one-to-one total quasi_total () () () () () () Element of bool [:NAT,NAT:]

(id NAT) * c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

n2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

h1 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]

n1 * h1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

h2 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]

n2 * h2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

h2 * h1 is non empty Relation-like NAT -defined NAT -valued RAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]

(h2 * h1) * n2 is non empty Relation-like NAT -defined X -valued Function-like total set

X is set

[:NAT,X:] is Relation-like set

bool [:NAT,X:] is non empty set

c

c

NAT --> c

{c

[:NAT,{c

bool [:NAT,{c

n1 is Relation-like NAT -defined X -valued Function-like quasi_total Element of bool [:NAT,X:]

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

rng c

bool X is non empty set

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,c

rng n1 is non empty Element of bool X

n2 is set

h1 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]

c

h2 is set

n1 . h2 is set

h1 . h2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,c

rng n1 is non empty Element of bool X

bool X is non empty set

rng c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

[:X,c

bool [:X,c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

rng n1 is non empty Element of bool X

bool X is non empty set

n2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

h1 is Relation-like X -defined c

dom h1 is Element of bool X

h1 /* n2 is non empty Relation-like NAT -defined c

[:NAT,c

bool [:NAT,c

h1 /* n1 is non empty Relation-like NAT -defined c

h2 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]

(X,h2,n1) is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,n1)

h2 * (h1 /* n1) is non empty Relation-like NAT -defined c

X is non empty non empty-membered set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

NAT --> c

{c

[:NAT,{c

bool [:NAT,{c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

X is non empty non empty-membered set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,c

rng n1 is non empty Element of bool X

bool X is non empty set

rng c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

dom c

bool NAT is non empty set

n1 is Element of X

h1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

c

n2 is Element of X

n1 is Element of X

n2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

c

X is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

c

n1 is set

[:NAT,n1:] is Relation-like set

bool [:NAT,n1:] is non empty set

n2 is Relation-like NAT -defined n1 -valued Function-like constant quasi_total Element of bool [:NAT,n1:]

n2 . X is Element of n1

n2 . c

dom n2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

bool NAT is non empty set

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

dom c

bool NAT is non empty set

n1 is set

n2 is set

c

c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

h1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

h2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

c

n is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

c

n + 1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

c

c

c

n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

n2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

c

c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

n2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

c

n1 . n2 is set

h1 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]

(X,h1,c

n1 . n2 is Element of X

h1 . n2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

c

c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

[:X,c

bool [:X,c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

rng n1 is non empty Element of bool X

bool X is non empty set

n2 is Relation-like X -defined c

dom n2 is Element of bool X

n2 /* n1 is non empty Relation-like NAT -defined c

[:NAT,c

bool [:NAT,c

h1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

(c

(X,n1,h1) is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,n1)

n2 /* (X,n1,h1) is non empty Relation-like NAT -defined c

h2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

(c

(n2 /* (X,n1,h1)) . h2 is set

rng (X,n1,h1) is non empty Element of bool X

(c

h2 + h1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

(n2 /* n1) . (h2 + h1) is Element of c

n1 . (h2 + h1) is Element of X

n2 . (n1 . (h2 + h1)) is set

(X,n1,h1) . h2 is Element of X

n2 . ((X,n1,h1) . h2) is set

(n2 /* (X,n1,h1)) . h2 is Element of c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

rng c

bool X is non empty set

n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

c

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

[:X,c

bool [:X,c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

n2 is Relation-like X -defined c

n2 /* n1 is non empty Relation-like NAT -defined c

[:NAT,c

bool [:NAT,c

h1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

(X,n1,h1) is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,n1)

n2 /* (X,n1,h1) is non empty Relation-like NAT -defined c

(c

dom n2 is Element of bool X

bool X is non empty set

rng n1 is non empty Element of bool X

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

[:X,c

bool [:X,c

n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

rng n1 is non empty Element of bool X

bool X is non empty set

n2 is Relation-like X -defined c

dom n2 is Element of bool X

n2 .: (rng n1) is Element of bool c

bool c

n2 /* n1 is non empty Relation-like NAT -defined c

[:NAT,c

bool [:NAT,c

rng (n2 /* n1) is non empty Element of bool c

h1 is Element of c

h2 is Element of X

n2 . h2 is set

n is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

n1 . n is Element of X

(n2 /* n1) . n is Element of c

h2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

(n2 /* n1) . h2 is Element of c

n1 . h2 is Element of X

n2 . (n1 . h2) is set

X is non empty set

[:NAT,X:] is non empty Relation-like set

bool [:NAT,X:] is non empty set

c

[:X,c

bool [:X,c

n1 is set

[:c

bool [:c

n2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]

rng n2 is non empty Element of bool X

bool X is non empty set

h1 is Relation-like X -defined c

h1 /* n2 is non empty Relation-like NAT -defined c

[:NAT,c

bool [:NAT,c

h2 is Relation-like c

h2 * h1 is Relation-like X -defined n1 -valued Function-like Element of bool [:X,n1:]

[:X,n1:] is Relation-like set

bool [:X,n1:] is non empty set

dom (h2 * h1) is Element of bool X

h2 /* (h1 /* n2) is Relation-like NAT -defined n1 -valued Function-like quasi_total Element of bool [:NAT,n1:]

[:NAT,n1:] is Relation-like set

bool [:NAT,n1:] is non empty set

(h2 * h1) /* n2 is Relation-like NAT -defined n1 -valued Function-like quasi_total Element of bool [:NAT,n1:]

dom h1 is Element of bool X

h1 .: (rng n2) is Element of bool c

bool c

dom h2 is Element of bool c

rng (h1 /* n2) is non empty Element of bool c

n is complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real Element of NAT

n2 . n is Element of X

((h2 * h1) /* n2) . n is Element of n1

(h2 * h1) . (n2 . n) is set

h1 . (n2 . n) is set

h2 . (h1 . (n2 . n)) is set

(h1 /* n2) . n is Element of c

h2 . ((h1 /* n2) . n) is set

(h2 /* (h1 /* n2)) . n is Element of n1

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is Relation-like set

rng X is set

X is non empty Relation-like NAT -defined Function-like total set

dom X is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

bool NAT is non empty set

X . 0 is set

n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set

X . n1 is set

c

c

n1 is set

dom X is non empty set

n2 is set

X . n1 is set

X . n2 is set

c

n1 is non empty Relation-like NAT -defined Function-like total (c

rng n1 is non empty set

rng c

X is set

X --> 0 is Relation-like X -defined NAT -valued RAT -valued INT -valued Function-like constant total quasi_total Function-yielding V40() () () () () Element of bool [:X,NAT:]

[:X,NAT:] is Relation-like RAT -valued INT -valued () () () () set

bool [:X,NAT:] is non empty set

{0} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered functional set

[:X,{0}:] is Relation-like RAT -valued INT -valued () () () () set