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
c2 is Relation-like () set
rng X is set
rng c2 is complex-membered set
X is Relation-like set
c2 is Relation-like () set
rng X is set
rng c2 is ext-real-membered set
X is Relation-like set
c2 is Relation-like () () () set
rng X is set
rng c2 is complex-membered ext-real-membered real-membered set
X is Relation-like set
c2 is Relation-like RAT -valued () () () set
X is Relation-like set
c2 is Relation-like INT -valued () () () set
X is Relation-like set
c2 is Relation-like RAT -valued () () () () set
rng X is set
rng c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
X is Relation-like () set
bool X is non empty set
c2 is Relation-like Element of bool X
X is Relation-like () set
bool X is non empty set
c2 is Relation-like Element of bool X
X is Relation-like () () () set
bool X is non empty set
c2 is Relation-like () () Element of bool X
X is Relation-like RAT -valued () () () set
bool X is non empty set
c2 is Relation-like RAT -valued () () () Element of bool X
X is Relation-like INT -valued () () () set
bool X is non empty set
c2 is Relation-like INT -valued () () () Element of bool X
X is Relation-like RAT -valued () () () () set
bool X is non empty set
c2 is Relation-like RAT -valued () () () Element of bool X
X is Relation-like () set
c2 is Relation-like () set
X \/ c2 is Relation-like set
rng (X \/ c2) is set
rng X is complex-membered set
rng c2 is complex-membered set
(rng X) \/ (rng c2) is complex-membered set
X is Relation-like () set
c2 is Relation-like () set
X \/ c2 is Relation-like set
rng (X \/ c2) is set
rng X is ext-real-membered set
rng c2 is ext-real-membered set
(rng X) \/ (rng c2) is ext-real-membered set
X is Relation-like () () () set
c2 is Relation-like () () () set
X \/ c2 is Relation-like () () set
rng (X \/ c2) is complex-membered ext-real-membered set
rng X is complex-membered ext-real-membered real-membered set
rng c2 is complex-membered ext-real-membered real-membered set
(rng X) \/ (rng c2) is complex-membered ext-real-membered real-membered set
X is Relation-like RAT -valued () () () set
c2 is Relation-like RAT -valued () () () set
X \/ c2 is Relation-like RAT -valued () () () set
X is Relation-like INT -valued () () () set
c2 is Relation-like INT -valued () () () set
X \/ c2 is Relation-like INT -valued () () () set
X is Relation-like RAT -valued () () () () set
c2 is Relation-like RAT -valued () () () () set
X \/ c2 is Relation-like RAT -valued () () () set
rng (X \/ c2) is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
rng c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
(rng X) \/ (rng c2) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
X is Relation-like () set
c2 is Relation-like set
X /\ c2 is Relation-like set
rng (X /\ c2) is set
rng X is complex-membered set
X \ c2 is Relation-like () Element of bool X
bool X is non empty set
X is Relation-like () set
c2 is Relation-like set
X /\ c2 is Relation-like set
rng (X /\ c2) is set
rng X is ext-real-membered set
X \ c2 is Relation-like () Element of bool X
bool X is non empty set
X is Relation-like () () () set
c2 is Relation-like set
X /\ c2 is Relation-like () () set
rng (X /\ c2) is complex-membered ext-real-membered set
rng X is complex-membered ext-real-membered real-membered set
X \ c2 is Relation-like () () () Element of bool X
bool X is non empty set
X is Relation-like RAT -valued () () () set
c2 is Relation-like set
X /\ c2 is Relation-like RAT -valued () () () set
X \ c2 is Relation-like RAT -valued () () () Element of bool X
bool X is non empty set
X is Relation-like INT -valued () () () set
c2 is Relation-like set
X /\ c2 is Relation-like INT -valued () () () set
X \ c2 is Relation-like INT -valued () () () Element of bool X
bool X is non empty set
X is Relation-like RAT -valued () () () () set
c2 is Relation-like set
X /\ c2 is Relation-like RAT -valued () () () set
rng (X /\ c2) is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
X \ c2 is Relation-like RAT -valued () () () () Element of bool X
bool X is non empty set
X is Relation-like () set
c2 is Relation-like () set
X \+\ c2 is Relation-like set
X \ c2 is Relation-like () set
c2 \ X is Relation-like () set
(X \ c2) \/ (c2 \ X) is Relation-like () set
X is Relation-like () set
c2 is Relation-like () set
X \+\ c2 is Relation-like set
X \ c2 is Relation-like () set
c2 \ X is Relation-like () set
(X \ c2) \/ (c2 \ X) is Relation-like () set
X is Relation-like () () () set
c2 is Relation-like () () () set
X \+\ c2 is Relation-like () () set
X \ c2 is Relation-like () () () set
c2 \ X is Relation-like () () () set
(X \ c2) \/ (c2 \ X) is Relation-like () () () set
X is Relation-like RAT -valued () () () set
c2 is Relation-like RAT -valued () () () set
X \+\ c2 is Relation-like () () () set
X \ c2 is Relation-like RAT -valued () () () set
c2 \ X is Relation-like RAT -valued () () () set
(X \ c2) \/ (c2 \ X) is Relation-like RAT -valued () () () set
X is Relation-like INT -valued () () () set
c2 is Relation-like INT -valued () () () set
X \+\ c2 is Relation-like () () () set
X \ c2 is Relation-like INT -valued () () () set
c2 \ X is Relation-like INT -valued () () () set
(X \ c2) \/ (c2 \ X) is Relation-like INT -valued () () () set
X is Relation-like RAT -valued () () () () set
c2 is Relation-like RAT -valued () () () () set
X \+\ c2 is Relation-like RAT -valued () () () set
X \ c2 is Relation-like RAT -valued () () () () set
c2 \ X is Relation-like RAT -valued () () () () set
(X \ c2) \/ (c2 \ X) is Relation-like RAT -valued () () () () set
X is Relation-like () set
c2 is set
X .: c2 is set
rng X is complex-membered set
X is Relation-like () set
c2 is set
X .: c2 is set
rng X is ext-real-membered set
X is Relation-like () () () set
c2 is set
X .: c2 is complex-membered ext-real-membered set
rng X is complex-membered ext-real-membered real-membered set
X is Relation-like RAT -valued () () () set
c2 is set
X .: c2 is complex-membered ext-real-membered real-membered set
rng X is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
X is Relation-like INT -valued () () () set
c2 is set
X .: c2 is complex-membered ext-real-membered real-membered set
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
c2 is set
X .: c2 is complex-membered ext-real-membered real-membered rational-membered set
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
c2 is set
Im (X,c2) is set
{c2} is non empty trivial set
X .: {c2} is complex-membered set
X is Relation-like () set
c2 is set
Im (X,c2) is set
{c2} is non empty trivial set
X .: {c2} is ext-real-membered set
X is Relation-like () () () set
c2 is set
Im (X,c2) is complex-membered ext-real-membered set
{c2} is non empty trivial set
X .: {c2} is complex-membered ext-real-membered real-membered set
X is Relation-like RAT -valued () () () set
c2 is set
Im (X,c2) is complex-membered ext-real-membered real-membered set
{c2} is non empty trivial set
X .: {c2} is complex-membered ext-real-membered real-membered rational-membered set
X is Relation-like INT -valued () () () set
c2 is set
Im (X,c2) is complex-membered ext-real-membered real-membered set
{c2} is non empty trivial set
X .: {c2} is complex-membered ext-real-membered real-membered rational-membered integer-membered set
X is Relation-like RAT -valued () () () () set
c2 is set
Im (X,c2) is complex-membered ext-real-membered real-membered rational-membered set
{c2} is non empty trivial set
X .: {c2} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
X is Relation-like () set
c2 is set
X | c2 is Relation-like set
rng X is complex-membered set
rng (X | c2) is set
X is Relation-like () set
c2 is set
X | c2 is Relation-like set
rng X is ext-real-membered set
rng (X | c2) is set
X is Relation-like () () () set
c2 is set
X | c2 is Relation-like () () set
rng X is complex-membered ext-real-membered real-membered set
rng (X | c2) is complex-membered ext-real-membered set
X is Relation-like RAT -valued () () () set
c2 is set
X | c2 is Relation-like RAT -valued () () () set
X is Relation-like INT -valued () () () set
c2 is set
X | c2 is Relation-like INT -valued () () () set
X is Relation-like RAT -valued () () () () set
c2 is set
X | c2 is Relation-like RAT -valued () () () set
rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
rng (X | c2) is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
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
c2 is Relation-like () set
X * c2 is Relation-like set
rng c2 is complex-membered set
rng (X * c2) is set
X is Relation-like set
c2 is Relation-like () set
X * c2 is Relation-like set
rng c2 is ext-real-membered set
rng (X * c2) is set
X is Relation-like set
c2 is Relation-like () () () set
X * c2 is Relation-like () () set
rng c2 is complex-membered ext-real-membered real-membered set
rng (X * c2) is complex-membered ext-real-membered set
X is Relation-like set
c2 is Relation-like RAT -valued () () () set
X * c2 is Relation-like RAT -valued () () () set
X is Relation-like set
c2 is Relation-like INT -valued () () () set
X * c2 is Relation-like INT -valued () () () set
X is Relation-like set
c2 is Relation-like RAT -valued () () () () set
X * c2 is Relation-like RAT -valued () () () set
rng c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
rng (X * c2) is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
X is Relation-like Function-like set
dom X is set
c2 is set
X . c2 is set
n1 is Relation-like Function-like () set
n1 . c2 is set
rng n1 is complex-membered set
c2 is set
rng X is set
n1 is set
X . n1 is set
c2 is set
X . c2 is set
n1 is Relation-like Function-like () set
n1 . c2 is set
rng n1 is ext-real-membered set
c2 is set
rng X is set
n1 is set
X . n1 is set
c2 is set
X . c2 is set
n1 is Relation-like Function-like () () () set
n1 . c2 is set
rng n1 is complex-membered ext-real-membered real-membered set
c2 is set
rng X is set
n1 is set
X . n1 is set
c2 is set
X . c2 is set
n1 is Relation-like RAT -valued Function-like () () () () set
n1 . c2 is set
rng n1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
c2 is set
rng X is set
n1 is set
X . n1 is set
X is Relation-like Function-like set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
dom X is set
c2 is set
X . c2 is set
X is Relation-like Function-like set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
dom X is set
c2 is set
X . c2 is set
X is Relation-like Function-like set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
dom X is set
c2 is set
X . c2 is set
X is Relation-like Function-like set
c2 is set
dom X is set
X . c2 is set
rng X is set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
c2 is set
rng X is set
dom X is set
n1 is set
X . n1 is set
X is Relation-like Function-like set
c2 is set
dom X is set
X . c2 is set
rng X is set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
c2 is set
rng X is set
dom X is set
n1 is set
X . n1 is set
X is Relation-like Function-like set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
X . c2 is set
c2 is set
dom X is set
dom X is set
c2 is set
X . c2 is set
X is Relation-like Function-like () set
c2 is set
X . c2 is set
X is Relation-like Function-like () set
c2 is set
X . c2 is set
X is Relation-like Function-like () () () set
c2 is set
X . c2 is complex ext-real set
X is Relation-like RAT -valued Function-like () () () set
c2 is set
X . c2 is complex real ext-real set
X is Relation-like INT -valued Function-like () () () set
c2 is set
X . c2 is complex real ext-real set
X is Relation-like RAT -valued Function-like () () () () set
c2 is set
X . c2 is complex real rational ext-real set
X is set
c2 is complex set
X --> c2 is Relation-like X -defined {c2} -valued Function-like constant total quasi_total Element of bool [:X,{c2}:]
{c2} is non empty trivial complex-membered set
[:X,{c2}:] is Relation-like set
bool [:X,{c2}:] is non empty set
rng (X --> c2) is trivial complex-membered Element of bool {c2}
bool {c2} is non empty set
X is set
c2 is ext-real set
X --> c2 is Relation-like X -defined {c2} -valued Function-like constant total quasi_total Element of bool [:X,{c2}:]
{c2} is non empty trivial ext-real-membered set
[:X,{c2}:] is Relation-like set
bool [:X,{c2}:] is non empty set
rng (X --> c2) is trivial ext-real-membered Element of bool {c2}
bool {c2} is non empty set
X is set
c2 is complex real ext-real set
X --> c2 is Relation-like X -defined {c2} -valued Function-like constant total quasi_total () () Element of bool [:X,{c2}:]
{c2} is non empty trivial complex-membered ext-real-membered real-membered set
[:X,{c2}:] is Relation-like set
bool [:X,{c2}:] is non empty set
rng (X --> c2) is trivial complex-membered ext-real-membered real-membered Element of bool {c2}
bool {c2} is non empty set
X is set
c2 is complex real rational ext-real set
X --> c2 is Relation-like X -defined {c2} -valued Function-like constant total quasi_total () () () Element of bool [:X,{c2}:]
{c2} is non empty trivial complex-membered ext-real-membered real-membered rational-membered set
[:X,{c2}:] is Relation-like set
bool [:X,{c2}:] is non empty set
rng (X --> c2) is trivial complex-membered ext-real-membered real-membered rational-membered Element of bool {c2}
bool {c2} is non empty set
X is set
c2 is complex real integer rational ext-real set
X --> c2 is Relation-like X -defined RAT -valued {c2} -valued Function-like constant total quasi_total () () () Element of bool [:X,{c2}:]
{c2} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered set
[:X,{c2}:] is Relation-like set
bool [:X,{c2}:] is non empty set
rng (X --> c2) is trivial complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool {c2}
bool {c2} is non empty set
X is set
c2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
X --> c2 is Relation-like X -defined RAT -valued INT -valued {c2} -valued Function-like constant total quasi_total () () () Element of bool [:X,{c2}:]
{c2} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
[:X,{c2}:] is Relation-like set
bool [:X,{c2}:] is non empty set
rng (X --> c2) is trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool {c2}
bool {c2} is non empty set
X is Relation-like Function-like () set
c2 is Relation-like Function-like () set
X +* c2 is Relation-like Function-like set
rng (X +* c2) is set
rng X is complex-membered set
rng c2 is complex-membered set
(rng X) \/ (rng c2) is complex-membered set
X is Relation-like Function-like () set
c2 is Relation-like Function-like () set
X +* c2 is Relation-like Function-like set
rng (X +* c2) is set
rng X is ext-real-membered set
rng c2 is ext-real-membered set
(rng X) \/ (rng c2) is ext-real-membered set
X is Relation-like Function-like () () () set
c2 is Relation-like Function-like () () () set
X +* c2 is Relation-like Function-like () () set
rng (X +* c2) is complex-membered ext-real-membered set
rng X is complex-membered ext-real-membered real-membered set
rng c2 is complex-membered ext-real-membered real-membered set
(rng X) \/ (rng c2) is complex-membered ext-real-membered real-membered set
X is Relation-like RAT -valued Function-like () () () set
c2 is Relation-like RAT -valued Function-like () () () set
X +* c2 is Relation-like Function-like () () () set
rng (X +* c2) is complex-membered ext-real-membered real-membered set
rng X is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
rng c2 is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
(rng X) \/ (rng c2) is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
X is Relation-like INT -valued Function-like () () () set
c2 is Relation-like INT -valued Function-like () () () set
X +* c2 is Relation-like Function-like () () () set
rng (X +* c2) is complex-membered ext-real-membered real-membered set
rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool INT
rng c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool INT
(rng X) \/ (rng c2) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool INT
X is Relation-like RAT -valued Function-like () () () () set
c2 is Relation-like RAT -valued Function-like () () () () set
X +* c2 is Relation-like RAT -valued Function-like () () () set
rng (X +* c2) is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
rng X is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
rng c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
(rng X) \/ (rng c2) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool RAT
X is set
c2 is complex set
X .--> c2 is Relation-like {X} -defined Function-like one-to-one set
{X} is non empty trivial set
{X} --> c2 is non empty Relation-like {X} -defined {c2} -valued Function-like constant total quasi_total () Element of bool [:{X},{c2}:]
{c2} is non empty trivial complex-membered set
[:{X},{c2}:] is non empty Relation-like set
bool [:{X},{c2}:] is non empty set
X is set
c2 is ext-real set
X .--> c2 is Relation-like {X} -defined Function-like one-to-one set
{X} is non empty trivial set
{X} --> c2 is non empty Relation-like {X} -defined {c2} -valued Function-like constant total quasi_total () Element of bool [:{X},{c2}:]
{c2} is non empty trivial ext-real-membered set
[:{X},{c2}:] is non empty Relation-like set
bool [:{X},{c2}:] is non empty set
X is set
c2 is complex real ext-real set
X .--> c2 is Relation-like {X} -defined Function-like one-to-one () () set
{X} is non empty trivial set
{X} --> c2 is non empty Relation-like {X} -defined {c2} -valued Function-like constant total quasi_total () () () Element of bool [:{X},{c2}:]
{c2} is non empty trivial complex-membered ext-real-membered real-membered set
[:{X},{c2}:] is non empty Relation-like set
bool [:{X},{c2}:] is non empty set
X is set
c2 is complex real rational ext-real set
X .--> c2 is Relation-like {X} -defined Function-like one-to-one () () () set
{X} is non empty trivial set
{X} --> c2 is non empty Relation-like {X} -defined RAT -valued {c2} -valued Function-like constant total quasi_total () () () Element of bool [:{X},{c2}:]
{c2} is non empty trivial complex-membered ext-real-membered real-membered rational-membered set
[:{X},{c2}:] is non empty Relation-like set
bool [:{X},{c2}:] is non empty set
X is set
c2 is complex real integer rational ext-real set
X .--> c2 is Relation-like {X} -defined RAT -valued Function-like one-to-one () () () set
{X} is non empty trivial set
{X} --> c2 is non empty Relation-like {X} -defined RAT -valued INT -valued {c2} -valued Function-like constant total quasi_total () () () Element of bool [:{X},{c2}:]
{c2} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered set
[:{X},{c2}:] is non empty Relation-like set
bool [:{X},{c2}:] is non empty set
X is set
c2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
X .--> c2 is Relation-like {X} -defined RAT -valued INT -valued Function-like one-to-one () () () set
{X} is non empty trivial set
{X} --> c2 is non empty Relation-like {X} -defined RAT -valued INT -valued {c2} -valued Function-like constant total quasi_total () () () () Element of bool [:{X},{c2}:]
{c2} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
[:{X},{c2}:] is non empty Relation-like set
bool [:{X},{c2}:] is non empty set
X is set
c2 is complex-membered set
[:X,c2:] is Relation-like set
bool [:X,c2:] is non empty set
n1 is Relation-like X -defined c2 -valued Element of bool [:X,c2:]
rng n1 is complex-membered Element of bool c2
bool c2 is non empty set
X is set
c2 is ext-real-membered set
[:X,c2:] is Relation-like set
bool [:X,c2:] is non empty set
n1 is Relation-like X -defined c2 -valued Element of bool [:X,c2:]
rng n1 is ext-real-membered Element of bool c2
bool c2 is non empty set
X is set
c2 is complex-membered ext-real-membered real-membered set
[:X,c2:] is Relation-like set
bool [:X,c2:] is non empty set
n1 is Relation-like X -defined c2 -valued () () Element of bool [:X,c2:]
rng n1 is complex-membered ext-real-membered real-membered Element of bool c2
bool c2 is non empty set
X is set
c2 is complex-membered ext-real-membered real-membered rational-membered set
[:X,c2:] is Relation-like set
bool [:X,c2:] is non empty set
n1 is Relation-like X -defined c2 -valued () () () Element of bool [:X,c2:]
rng n1 is complex-membered ext-real-membered real-membered rational-membered Element of bool c2
bool c2 is non empty set
X is set
c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered set
[:X,c2:] is Relation-like set
bool [:X,c2:] is non empty set
n1 is Relation-like X -defined c2 -valued () () () Element of bool [:X,c2:]
rng n1 is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool c2
bool c2 is non empty set
X is set
c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
[:X,c2:] is Relation-like set
bool [:X,c2:] is non empty set
n1 is Relation-like X -defined c2 -valued () () () Element of bool [:X,c2:]
rng n1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool c2
bool c2 is non empty set
X is set
c2 is complex-membered set
[:X,c2:] is Relation-like set
rng [:X,c2:] is set
X is set
c2 is ext-real-membered set
[:X,c2:] is Relation-like set
rng [:X,c2:] is set
X is set
c2 is complex-membered ext-real-membered real-membered set
[:X,c2:] is Relation-like () () set
rng [:X,c2:] is complex-membered ext-real-membered set
X is set
c2 is complex-membered ext-real-membered real-membered rational-membered set
[:X,c2:] is Relation-like () () () set
rng [:X,c2:] is complex-membered ext-real-membered real-membered set
X is set
c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered set
[:X,c2:] is Relation-like RAT -valued () () () set
rng [:X,c2:] is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT
X is set
c2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
[:X,c2:] is Relation-like RAT -valued INT -valued () () () set
rng [:X,c2:] is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool RAT
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
c2 is set
n1 is set
X . n1 is complex set
X is non empty Relation-like Function-like constant () set
dom X is non empty set
c2 is set
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
c2 is set
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
c2 is set
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
c2 is set
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
c2 is set
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
c2 is ext-real set
dom X is set
X . c2 is ext-real set
n1 is ext-real set
X . n1 is ext-real set
c2 is ext-real set
dom X is set
X . c2 is ext-real set
n1 is ext-real set
X . n1 is ext-real set
X is Relation-like Function-like () set
c2 is ext-real set
dom X is set
X . c2 is ext-real set
n1 is ext-real set
X . n1 is ext-real set
X is Relation-like Function-like () set
c2 is ext-real set
dom X is set
X . c2 is ext-real set
n1 is ext-real set
X . n1 is ext-real set
X is Relation-like Function-like () () () set
c2 is Relation-like Function-like () () () set
X * c2 is Relation-like Function-like () set
n1 is ext-real set
dom (X * c2) is set
(X * c2) . n1 is ext-real set
n2 is ext-real set
(X * c2) . n2 is ext-real set
dom X is set
X . n1 is ext-real set
c2 . (X . n1) is ext-real set
X . n2 is ext-real set
c2 . (X . n2) is ext-real set
dom c2 is set
X is Relation-like Function-like () () set
c2 is Relation-like Function-like () () set
X * c2 is Relation-like Function-like () set
n1 is ext-real set
dom (X * c2) is set
(X * c2) . n1 is ext-real set
n2 is ext-real set
(X * c2) . n2 is ext-real set
dom X is set
X . n1 is ext-real set
c2 . (X . n1) is ext-real set
X . n2 is ext-real set
c2 . (X . n2) is ext-real set
dom c2 is set
X is Relation-like Function-like () () () set
c2 is Relation-like Function-like () () () set
X * c2 is Relation-like Function-like () set
n1 is ext-real set
dom (X * c2) is set
(X * c2) . n1 is ext-real set
n2 is ext-real set
(X * c2) . n2 is ext-real set
dom X is set
X . n1 is ext-real set
c2 . (X . n1) is ext-real set
X . n2 is ext-real set
c2 . (X . n2) is ext-real set
dom c2 is set
X is Relation-like Function-like () () set
c2 is Relation-like Function-like () () set
X * c2 is Relation-like Function-like () set
n1 is ext-real set
dom (X * c2) is set
(X * c2) . n1 is ext-real set
n2 is ext-real set
(X * c2) . n2 is ext-real set
dom X is set
X . n1 is ext-real set
c2 . (X . n1) is ext-real set
X . n2 is ext-real set
c2 . (X . n2) is ext-real set
dom c2 is set
X is Relation-like Function-like () () () set
c2 is Relation-like Function-like () () () set
X * c2 is Relation-like Function-like () set
n1 is ext-real set
dom (X * c2) is set
(X * c2) . n1 is ext-real set
n2 is ext-real set
(X * c2) . n2 is ext-real set
dom X is set
X . n1 is ext-real set
c2 . (X . n1) is ext-real set
X . n2 is ext-real set
c2 . (X . n2) is ext-real set
dom c2 is set
c2 * X is Relation-like Function-like () set
n1 is ext-real set
dom (c2 * X) is set
(c2 * X) . n1 is ext-real set
n2 is ext-real set
(c2 * X) . n2 is ext-real set
dom c2 is set
c2 . n1 is ext-real set
X . (c2 . n1) is ext-real set
c2 . n2 is ext-real set
X . (c2 . n2) is ext-real set
dom X is set
X is Relation-like Function-like () () set
c2 is Relation-like Function-like () () set
X * c2 is Relation-like Function-like () set
n1 is ext-real set
dom (X * c2) is set
(X * c2) . n1 is ext-real set
n2 is ext-real set
(X * c2) . n2 is ext-real set
dom X is set
X . n1 is ext-real set
c2 . (X . n1) is ext-real set
X . n2 is ext-real set
c2 . (X . n2) is ext-real set
dom c2 is set
c2 * X is Relation-like Function-like () set
n1 is ext-real set
dom (c2 * X) is set
(c2 * X) . n1 is ext-real set
n2 is ext-real set
(c2 * X) . n2 is ext-real set
dom c2 is set
c2 . n1 is ext-real set
X . (c2 . n1) is ext-real set
c2 . n2 is ext-real set
X . (c2 . n2) is ext-real set
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:]
c2 is ext-real set
dom (id X) is set
(id X) . c2 is ext-real set
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
c2 is Relation-like X -defined X -valued Function-like total quasi_total () Element of bool [:X,X:]
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
c2 is non empty Relation-like NAT -defined Function-like total set
rng c2 is non empty set
n1 is non empty Relation-like NAT -defined Function-like total (c2)
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 * c2 is non empty Relation-like NAT -defined Function-like total set
X is non empty set
c2 is non empty Relation-like NAT -defined X -valued Function-like total set
n1 is non empty Relation-like NAT -defined Function-like total (c2)
rng n1 is non empty set
rng c2 is non empty Element of bool X
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
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
n1 is non empty Relation-like NAT -defined X -valued Function-like total (c2)
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
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
c2 ^\ n1 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) ^\ 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
c2 ^\ n1 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:]
h1 * c2 is non empty Relation-like NAT -defined X -valued Function-like total set
c2 * (id NAT) is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
(c2 * (id NAT)) ^\ n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
c2 * h1 is non empty Relation-like NAT -defined X -valued Function-like total 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
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
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) * c2 is non empty Relation-like NAT -defined X -valued Function-like total set
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
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
c2 is Relation-like NAT -defined X -valued Function-like quasi_total Element of bool [:NAT,X:]
c2 is set
NAT --> c2 is non empty Relation-like NAT -defined {c2} -valued Function-like constant total quasi_total Element of bool [:NAT,{c2}:]
{c2} is non empty trivial set
[:NAT,{c2}:] is non empty Relation-like set
bool [:NAT,{c2}:] is non empty set
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
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
rng c2 is non empty Element of bool X
bool X is non empty set
n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,c2)
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:]
c2 * h1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
h2 is set
n1 . h2 is set
h1 . h2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
c2 . (h1 . h2) is Element of X
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty Relation-like NAT -defined X -valued Function-like constant total quasi_total Element of bool [:NAT,X:]
n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,c2)
rng n1 is non empty Element of bool X
bool X is non empty set
rng c2 is non empty trivial Element of bool X
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total () () () () () () Element of bool [:NAT,NAT:]
n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
c2 * n1 is non empty Relation-like NAT -defined X -valued Function-like total set
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty set
[:X,c2:] is non empty Relation-like set
bool [:X,c2:] is non empty set
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 c2 -valued Function-like Element of bool [:X,c2:]
dom h1 is Element of bool X
h1 /* n2 is non empty Relation-like NAT -defined c2 -valued Function-like total quasi_total Element of bool [:NAT,c2:]
[:NAT,c2:] is non empty Relation-like set
bool [:NAT,c2:] is non empty set
h1 /* n1 is non empty Relation-like NAT -defined c2 -valued Function-like total quasi_total Element of bool [:NAT,c2:]
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 c2 -valued Function-like total set
X is non empty non empty-membered set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty set
NAT --> c2 is non empty Relation-like non-empty non empty-yielding NAT -defined {c2} -valued Function-like constant total quasi_total Element of bool [:NAT,{c2}:]
{c2} is non empty trivial with_non-empty_elements non empty-membered set
[:NAT,{c2}:] is non empty Relation-like set
bool [:NAT,{c2}:] is non empty set
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
c2 is non empty Relation-like non-empty non empty-yielding NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
n1 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,c2)
rng n1 is non empty Element of bool X
bool X is non empty set
rng c2 is non empty with_non-empty_elements non empty-membered Element of bool X
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
dom c2 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
n1 is Element of X
h1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
c2 . h1 is Element of X
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
c2 . n2 is set
X is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
c2 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
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 . c2 is Element of n1
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
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
dom c2 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
n1 is set
n2 is set
c2 . n1 is set
c2 . n2 is set
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
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
c2 . h1 is Element of X
n is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
c2 . n is Element of X
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
c2 . (n + 1) is Element of X
c2 . 0 is Element of X
c2 . h2 is Element of X
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
c2 . n1 is Element of X
c2 . n2 is Element of X
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
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
c2 . n2 is set
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,c2) is non empty Relation-like NAT -defined X -valued Function-like total quasi_total (X,c2)
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
c2 . (h1 . n2) is Element of X
c2 . n2 is Element of X
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty set
[:X,c2:] is non empty Relation-like set
bool [:X,c2:] is non empty set
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 c2 -valued Function-like Element of bool [:X,c2:]
dom n2 is Element of bool X
n2 /* n1 is non empty Relation-like NAT -defined c2 -valued Function-like total quasi_total Element of bool [:NAT,c2:]
[:NAT,c2:] is non empty Relation-like set
bool [:NAT,c2:] is non empty set
h1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
(c2,(n2 /* n1),h1) is non empty Relation-like NAT -defined c2 -valued Function-like total quasi_total (c2,n2 /* n1)
(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 c2 -valued Function-like total quasi_total Element of bool [:NAT,c2:]
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
(c2,(n2 /* n1),h1) . h2 is set
(n2 /* (X,n1,h1)) . h2 is set
rng (X,n1,h1) is non empty Element of bool X
(c2,(n2 /* n1),h1) . h2 is Element of c2
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 c2
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 c2
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty Relation-like NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:]
rng c2 is non empty Element of bool X
bool X is non empty set
n1 is complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real set
c2 . n1 is Element of X
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty set
c2 is non empty set
[:X,c2:] is non empty Relation-like set
bool [:X,c2:] is non empty set
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 c2 -valued Function-like Element of bool [:X,c2:]
n2 /* n1 is non empty Relation-like NAT -defined c2 -valued Function-like total quasi_total Element of bool [:NAT,c2:]
[:NAT,c2:] is non empty Relation-like set
bool [:NAT,c2:] is non empty set
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 c2 -valued Function-like total quasi_total Element of bool [:NAT,c2:]
(c2,(n2 /* n1),h1) is non empty Relation-like NAT -defined c2 -valued Function-like total quasi_total (c2,n2 /* n1)
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
c2 is non empty set
[:X,c2:] is non empty Relation-like set
bool [:X,c2:] is non empty set
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 c2 -valued Function-like Element of bool [:X,c2:]
dom n2 is Element of bool X
n2 .: (rng n1) is Element of bool c2
bool c2 is non empty set
n2 /* n1 is non empty Relation-like NAT -defined c2 -valued Function-like total quasi_total Element of bool [:NAT,c2:]
[:NAT,c2:] is non empty Relation-like set
bool [:NAT,c2:] is non empty set
rng (n2 /* n1) is non empty Element of bool c2
h1 is Element of c2
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 c2
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 c2
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
c2 is non empty set
[:X,c2:] is non empty Relation-like set
bool [:X,c2:] is non empty set
n1 is set
[:c2,n1:] is Relation-like set
bool [:c2,n1:] is non empty set
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 c2 -valued Function-like Element of bool [:X,c2:]
h1 /* n2 is non empty Relation-like NAT -defined c2 -valued Function-like total quasi_total Element of bool [:NAT,c2:]
[:NAT,c2:] is non empty Relation-like set
bool [:NAT,c2:] is non empty set
h2 is Relation-like c2 -defined n1 -valued Function-like Element of bool [:c2,n1:]
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 c2
bool c2 is non empty set
dom h2 is Element of bool c2
rng (h1 /* n2) is non empty Element of bool c2
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 c2
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
c2 is set
c2 is set
n1 is set
dom X is non empty set
n2 is set
X . n1 is set
X . n2 is set
c2 is non empty Relation-like NAT -defined Function-like total set
n1 is non empty Relation-like NAT -defined Function-like total (c2)
rng n1 is non empty set
rng c2 is non empty set
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