:: COMSEQ_1 semantic presentation

REAL is non zero V47() V48() V49() V53() V54() set
NAT is non zero epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non zero V47() V53() V54() set
RAT is non zero V47() V48() V49() V50() V53() V54() set
INT is non zero V47() V48() V49() V50() V51() V53() V54() set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
1r is complex Element of COMPLEX
1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
|.1r.| is complex V31() V32() Element of REAL
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V47() V48() V49() V50() V51() V52() V53() set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
0 " is complex set
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
r is Relation-like Function-like set
dom r is set
seq is set
r . seq is set
rng r is set
seq is set
rng r is set
n is set
r . n is set
r is Relation-like Function-like set
dom r is set
seq is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
r . seq is set
seq is set
r . seq is set
r is set
seq is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
F₁(seq) is complex set
n is set
seq1 is set
r is Relation-like Function-like set
dom r is set
seq is set
r . seq is set
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
F₁(n) is complex set
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
n . seq1 is complex Element of COMPLEX
F₁(seq1) is complex set
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
F₁(n) is complex set
NAT --> 1r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
rng r is V47() Element of K19(COMPLEX)
K19(COMPLEX) is set
{1} is non zero V47() V48() V49() V50() V51() V52() set
0c is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V47() V48() V49() V50() V51() V52() V53() Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is set
r . seq is complex set
dom r is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
K19(NAT) is set
rng r is V47() Element of K19(COMPLEX)
K19(COMPLEX) is set
rng r is V47() Element of K19(COMPLEX)
K19(COMPLEX) is set
dom r is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
K19(NAT) is set
seq is set
r . seq is complex set
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
r . seq is complex Element of COMPLEX
seq is set
r . seq is complex set
{0c} is non zero V47() V48() V49() V50() V51() V52() set
COMPLEX \ {0c} is V47() Element of K19(COMPLEX)
K19(COMPLEX) is set
r is Relation-like non-empty NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
rng r is V47() Element of K19(COMPLEX)
r is complex Element of COMPLEX
{r} is non zero V47() set
seq is Relation-like Function-like set
dom seq is set
rng seq is set
n is set
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
rng n is V47() Element of K19(COMPLEX)
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r + seq) + n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq + n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + (seq + n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
((r + seq) + n) . seq1 is complex Element of COMPLEX
(r + seq) . seq1 is complex Element of COMPLEX
n . seq1 is complex Element of COMPLEX
((r + seq) . seq1) + (n . seq1) is complex Element of COMPLEX
r . seq1 is complex Element of COMPLEX
seq . seq1 is complex Element of COMPLEX
(r . seq1) + (seq . seq1) is complex Element of COMPLEX
((r . seq1) + (seq . seq1)) + (n . seq1) is complex Element of COMPLEX
(seq . seq1) + (n . seq1) is complex Element of COMPLEX
(r . seq1) + ((seq . seq1) + (n . seq1)) is complex Element of COMPLEX
(seq + n) . seq1 is complex Element of COMPLEX
(r . seq1) + ((seq + n) . seq1) is complex Element of COMPLEX
(r + (seq + n)) . seq1 is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
((r (#) seq) (#) n) . seq1 is complex Element of COMPLEX
(r (#) seq) . seq1 is complex Element of COMPLEX
n . seq1 is complex Element of COMPLEX
((r (#) seq) . seq1) * (n . seq1) is complex Element of COMPLEX
r . seq1 is complex Element of COMPLEX
seq . seq1 is complex Element of COMPLEX
(r . seq1) * (seq . seq1) is complex Element of COMPLEX
((r . seq1) * (seq . seq1)) * (n . seq1) is complex Element of COMPLEX
(seq . seq1) * (n . seq1) is complex Element of COMPLEX
(r . seq1) * ((seq . seq1) * (n . seq1)) is complex Element of COMPLEX
(seq (#) n) . seq1 is complex Element of COMPLEX
(r . seq1) * ((seq (#) n) . seq1) is complex Element of COMPLEX
(r (#) (seq (#) n)) . seq1 is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r + seq) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) n) + (seq (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
((r + seq) (#) n) . seq1 is complex Element of COMPLEX
(r + seq) . seq1 is complex Element of COMPLEX
n . seq1 is complex Element of COMPLEX
((r + seq) . seq1) * (n . seq1) is complex Element of COMPLEX
r . seq1 is complex Element of COMPLEX
seq . seq1 is complex Element of COMPLEX
(r . seq1) + (seq . seq1) is complex Element of COMPLEX
((r . seq1) + (seq . seq1)) * (n . seq1) is complex Element of COMPLEX
(r . seq1) * (n . seq1) is complex Element of COMPLEX
(seq . seq1) * (n . seq1) is complex Element of COMPLEX
((r . seq1) * (n . seq1)) + ((seq . seq1) * (n . seq1)) is complex Element of COMPLEX
(r (#) n) . seq1 is complex Element of COMPLEX
((r (#) n) . seq1) + ((seq . seq1) * (n . seq1)) is complex Element of COMPLEX
(seq (#) n) . seq1 is complex Element of COMPLEX
((r (#) n) . seq1) + ((seq (#) n) . seq1) is complex Element of COMPLEX
((r (#) n) + (seq (#) n)) . seq1 is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq + n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq + n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) + (r (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1r is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1 is non zero complex set
(- 1) (#) r is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1r) (#) r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r (#) (seq (#) n)) . seq1 is complex Element of COMPLEX
(seq (#) n) . seq1 is complex Element of COMPLEX
r * ((seq (#) n) . seq1) is complex Element of COMPLEX
seq . seq1 is complex Element of COMPLEX
n . seq1 is complex Element of COMPLEX
(seq . seq1) * (n . seq1) is complex Element of COMPLEX
r * ((seq . seq1) * (n . seq1)) is complex Element of COMPLEX
r * (seq . seq1) is complex Element of COMPLEX
(r * (seq . seq1)) * (n . seq1) is complex Element of COMPLEX
(r (#) seq) . seq1 is complex Element of COMPLEX
((r (#) seq) . seq1) * (n . seq1) is complex Element of COMPLEX
((r (#) seq) (#) n) . seq1 is complex Element of COMPLEX
r is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) (r (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r (#) (seq (#) n)) . seq1 is complex Element of COMPLEX
(seq (#) n) . seq1 is complex Element of COMPLEX
r * ((seq (#) n) . seq1) is complex Element of COMPLEX
seq . seq1 is complex Element of COMPLEX
n . seq1 is complex Element of COMPLEX
(seq . seq1) * (n . seq1) is complex Element of COMPLEX
r * ((seq . seq1) * (n . seq1)) is complex Element of COMPLEX
r * (n . seq1) is complex Element of COMPLEX
(seq . seq1) * (r * (n . seq1)) is complex Element of COMPLEX
(r (#) n) . seq1 is complex Element of COMPLEX
(seq . seq1) * ((r (#) n) . seq1) is complex Element of COMPLEX
(seq (#) (r (#) n)) . seq1 is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r - seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- 1 is non zero complex set
(- 1) (#) seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (- seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r - seq) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) n) - (seq (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (seq (#) n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) (seq (#) n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r (#) n) + (- (seq (#) n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- seq) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) n) + ((- seq) (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((- 1r) (#) seq) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) n) + (((- 1r) (#) seq) (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (seq (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) n) + ((- 1r) (#) (seq (#) n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) - (r (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (r (#) n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- 1 is non zero complex set
(- 1) (#) (r (#) n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r (#) seq) + (- (r (#) n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq - n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq - n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq + n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq + n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) + (r (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r (#) (seq + n)) . seq1 is complex Element of COMPLEX
(seq + n) . seq1 is complex Element of COMPLEX
r * ((seq + n) . seq1) is complex Element of COMPLEX
seq . seq1 is complex Element of COMPLEX
n . seq1 is complex Element of COMPLEX
(seq . seq1) + (n . seq1) is complex Element of COMPLEX
r * ((seq . seq1) + (n . seq1)) is complex Element of COMPLEX
r * (seq . seq1) is complex Element of COMPLEX
r * (n . seq1) is complex Element of COMPLEX
(r * (seq . seq1)) + (r * (n . seq1)) is complex Element of COMPLEX
(r (#) seq) . seq1 is complex Element of COMPLEX
((r (#) seq) . seq1) + (r * (n . seq1)) is complex Element of COMPLEX
(r (#) n) . seq1 is complex Element of COMPLEX
((r (#) seq) . seq1) + ((r (#) n) . seq1) is complex Element of COMPLEX
((r (#) seq) + (r (#) n)) . seq1 is complex Element of COMPLEX
r is complex Element of COMPLEX
seq is complex Element of COMPLEX
r * seq is complex Element of COMPLEX
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r * seq) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
((r * seq) (#) n) . seq1 is complex Element of COMPLEX
n . seq1 is complex Element of COMPLEX
(r * seq) * (n . seq1) is complex Element of COMPLEX
seq * (n . seq1) is complex Element of COMPLEX
r * (seq * (n . seq1)) is complex Element of COMPLEX
(seq (#) n) . seq1 is complex Element of COMPLEX
r * ((seq (#) n) . seq1) is complex Element of COMPLEX
(r (#) (seq (#) n)) . seq1 is complex Element of COMPLEX
r is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq - n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- 1 is non zero complex set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq - n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) - (r (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (r (#) n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) (r (#) n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r (#) seq) + (- (r (#) n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (- n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) + (r (#) (- n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) ((- 1r) (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) + (r (#) ((- 1r) (#) n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) * r is complex Element of COMPLEX
((- 1r) * r) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) + (((- 1r) * r) (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (r (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) + ((- 1r) (#) (r (#) n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq /" n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq (#) (n ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq /" n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) /" n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) (#) (n ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) (n ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq (#) (n ")) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r - seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- 1 is non zero complex set
(- 1) (#) seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (- seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq + n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r - (seq + n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (seq + n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) (seq + n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (- (seq + n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r - seq) - n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r - seq) + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1r) (#) (seq + n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + ((- 1r) (#) (seq + n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((- 1r) (#) seq) + ((- 1r) (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + (((- 1r) (#) seq) + ((- 1r) (#) n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- seq) + ((- 1r) (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + ((- seq) + ((- 1r) (#) n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- seq) + (- n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + ((- seq) + (- n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
1r (#) r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(1r (#) r) . seq is complex Element of COMPLEX
r . seq is complex Element of COMPLEX
1r * (r . seq) is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1 is non zero complex set
(- 1) (#) r is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- (- r) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) (#) (- r) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1 is non zero complex set
(- 1) (#) seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r - (- seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (- seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) (- seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (- (- seq)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r - seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- 1 is non zero complex set
(- 1) (#) seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (- seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq - n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r - (seq - n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (seq - n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) (seq - n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (- (seq - n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r - seq) + n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (seq - n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + ((- 1r) (#) (seq - n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((- 1r) (#) seq) - ((- 1r) (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- ((- 1r) (#) n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) ((- 1r) (#) n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
((- 1r) (#) seq) + (- ((- 1r) (#) n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (((- 1r) (#) seq) - ((- 1r) (#) n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- seq) - ((- 1r) (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- seq) + (- ((- 1r) (#) n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + ((- seq) - ((- 1r) (#) n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- seq) - (- n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- seq) + (- (- n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + ((- seq) - (- n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq - n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- 1 is non zero complex set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (seq - n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r + seq) - n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r + seq) + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq + (- n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + (seq + (- n)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1 is non zero complex set
(- 1) (#) r is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- r) (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (r (#) seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) (#) (r (#) seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) (#) seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (- seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((- 1r) (#) r) (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (r (#) seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) ((- 1r) (#) seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r ") . seq is complex Element of COMPLEX
r . seq is complex Element of COMPLEX
(r . seq) " is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r (#) seq) . n is complex Element of COMPLEX
r . n is complex Element of COMPLEX
seq . n is complex Element of COMPLEX
(r . n) * (seq . n) is complex Element of COMPLEX
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r (#) seq) . n is complex Element of COMPLEX
r . n is complex Element of COMPLEX
seq . n is complex Element of COMPLEX
(r . n) * (seq . n) is complex Element of COMPLEX
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r (#) seq) . n is complex Element of COMPLEX
r . n is complex Element of COMPLEX
seq . n is complex Element of COMPLEX
(r . n) * (seq . n) is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r ") (#) (seq ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
((r ") (#) (seq ")) . n is complex Element of COMPLEX
(r ") . n is complex Element of COMPLEX
(seq ") . n is complex Element of COMPLEX
((r ") . n) * ((seq ") . n) is complex Element of COMPLEX
seq . n is complex Element of COMPLEX
(seq . n) " is complex Element of COMPLEX
((r ") . n) * ((seq . n) ") is complex Element of COMPLEX
r . n is complex Element of COMPLEX
(r . n) " is complex Element of COMPLEX
((r . n) ") * ((seq . n) ") is complex Element of COMPLEX
(r . n) * (seq . n) is complex Element of COMPLEX
((r . n) * (seq . n)) " is complex Element of COMPLEX
(r (#) seq) . n is complex Element of COMPLEX
((r (#) seq) . n) " is complex Element of COMPLEX
((r (#) seq) ") . n is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq /" r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq (#) (r ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(seq /" r) (#) r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
r . n is complex Element of COMPLEX
((seq /" r) (#) r) . n is complex Element of COMPLEX
r " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) (r ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq (#) (r ")) . n is complex Element of COMPLEX
((seq (#) (r ")) . n) * (r . n) is complex Element of COMPLEX
seq . n is complex Element of COMPLEX
(r ") . n is complex Element of COMPLEX
(seq . n) * ((r ") . n) is complex Element of COMPLEX
((seq . n) * ((r ") . n)) * (r . n) is complex Element of COMPLEX
(r . n) " is complex Element of COMPLEX
(seq . n) * ((r . n) ") is complex Element of COMPLEX
((seq . n) * ((r . n) ")) * (r . n) is complex Element of COMPLEX
((r . n) ") * (r . n) is complex Element of COMPLEX
(seq . n) * (((r . n) ") * (r . n)) is complex Element of COMPLEX
(seq . n) * 1r is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n /" seq1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n (#) (seq1 ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r /" seq) (#) (n /" seq1) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) seq1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) n) /" (seq (#) seq1) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq (#) seq1) " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r (#) n) (#) ((seq (#) seq1) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
((r /" seq) (#) (n /" seq1)) . n is complex Element of COMPLEX
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) (seq ")) . n is complex Element of COMPLEX
(n /" seq1) . n is complex Element of COMPLEX
((r (#) (seq ")) . n) * ((n /" seq1) . n) is complex Element of COMPLEX
r . n is complex Element of COMPLEX
(seq ") . n is complex Element of COMPLEX
(r . n) * ((seq ") . n) is complex Element of COMPLEX
seq1 " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n (#) (seq1 ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(n (#) (seq1 ")) . n is complex Element of COMPLEX
((r . n) * ((seq ") . n)) * ((n (#) (seq1 ")) . n) is complex Element of COMPLEX
n . n is complex Element of COMPLEX
(seq1 ") . n is complex Element of COMPLEX
(n . n) * ((seq1 ") . n) is complex Element of COMPLEX
((r . n) * ((seq ") . n)) * ((n . n) * ((seq1 ") . n)) is complex Element of COMPLEX
((seq ") . n) * ((seq1 ") . n) is complex Element of COMPLEX
(n . n) * (((seq ") . n) * ((seq1 ") . n)) is complex Element of COMPLEX
(r . n) * ((n . n) * (((seq ") . n) * ((seq1 ") . n))) is complex Element of COMPLEX
(seq ") (#) (seq1 ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((seq ") (#) (seq1 ")) . n is complex Element of COMPLEX
(n . n) * (((seq ") (#) (seq1 ")) . n) is complex Element of COMPLEX
(r . n) * ((n . n) * (((seq ") (#) (seq1 ")) . n)) is complex Element of COMPLEX
(r . n) * (n . n) is complex Element of COMPLEX
((r . n) * (n . n)) * (((seq ") (#) (seq1 ")) . n) is complex Element of COMPLEX
(seq (#) seq1) " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((seq (#) seq1) ") . n is complex Element of COMPLEX
((r . n) * (n . n)) * (((seq (#) seq1) ") . n) is complex Element of COMPLEX
(r (#) n) . n is complex Element of COMPLEX
((r (#) n) . n) * (((seq (#) seq1) ") . n) is complex Element of COMPLEX
((r (#) n) /" (seq (#) seq1)) . n is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r /" seq) " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq /" r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq (#) (r ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
((r /" seq) ") . n is complex Element of COMPLEX
r " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq ") " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r ") (#) ((seq ") ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((r ") (#) ((seq ") ")) . n is complex Element of COMPLEX
(seq /" r) . n is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq /" n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq (#) (n ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq /" n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) /" n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) (#) (n ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) (#) (n ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq /" n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq (#) (n ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r /" (seq /" n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq /" n) " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) ((seq /" n) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) n) /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r (#) n) (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r /" (seq /" n)) . seq1 is complex Element of COMPLEX
n /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (n /" seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) (n /" seq)) . seq1 is complex Element of COMPLEX
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) n) (#) (seq ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((r (#) n) (#) (seq ")) . seq1 is complex Element of COMPLEX
((r (#) n) /" seq) . seq1 is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq /" n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq (#) (n ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n (#) r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq (#) r) /" (n (#) r) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(n (#) r) " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(seq (#) r) (#) ((n (#) r) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq1 is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
r . seq1 is complex Element of COMPLEX
(seq /" n) . seq1 is complex Element of COMPLEX
seq . seq1 is complex Element of COMPLEX
(seq . seq1) * 1r is complex Element of COMPLEX
n " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(n ") . seq1 is complex Element of COMPLEX
((seq . seq1) * 1r) * ((n ") . seq1) is complex Element of COMPLEX
(r . seq1) " is complex Element of COMPLEX
(r . seq1) * ((r . seq1) ") is complex Element of COMPLEX
(seq . seq1) * ((r . seq1) * ((r . seq1) ")) is complex Element of COMPLEX
((seq . seq1) * ((r . seq1) * ((r . seq1) "))) * ((n ") . seq1) is complex Element of COMPLEX
(seq . seq1) * (r . seq1) is complex Element of COMPLEX
((r . seq1) ") * ((n ") . seq1) is complex Element of COMPLEX
((seq . seq1) * (r . seq1)) * (((r . seq1) ") * ((n ") . seq1)) is complex Element of COMPLEX
(seq (#) r) . seq1 is complex Element of COMPLEX
((seq (#) r) . seq1) * (((r . seq1) ") * ((n ") . seq1)) is complex Element of COMPLEX
r " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r ") . seq1 is complex Element of COMPLEX
((r ") . seq1) * ((n ") . seq1) is complex Element of COMPLEX
((seq (#) r) . seq1) * (((r ") . seq1) * ((n ") . seq1)) is complex Element of COMPLEX
(n ") (#) (r ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((n ") (#) (r ")) . seq1 is complex Element of COMPLEX
((seq (#) r) . seq1) * (((n ") (#) (r ")) . seq1) is complex Element of COMPLEX
(n (#) r) " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((n (#) r) ") . seq1 is complex Element of COMPLEX
((seq (#) r) . seq1) * (((n (#) r) ") . seq1) is complex Element of COMPLEX
((seq (#) r) /" (n (#) r)) . seq1 is complex Element of COMPLEX
r is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
(r (#) seq) . n is complex Element of COMPLEX
seq . n is complex Element of COMPLEX
r * (seq . n) is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1 is non zero complex set
(- 1) (#) r is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- (- 1r) is complex Element of COMPLEX
r is complex Element of COMPLEX
r " is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r ") (#) (seq ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
((r (#) seq) ") . n is complex Element of COMPLEX
(r (#) seq) . n is complex Element of COMPLEX
((r (#) seq) . n) " is complex Element of COMPLEX
seq . n is complex Element of COMPLEX
r * (seq . n) is complex Element of COMPLEX
(r * (seq . n)) " is complex Element of COMPLEX
(seq . n) " is complex Element of COMPLEX
(r ") * ((seq . n) ") is complex Element of COMPLEX
(seq ") . n is complex Element of COMPLEX
(r ") * ((seq ") . n) is complex Element of COMPLEX
((r ") (#) (seq ")) . n is complex Element of COMPLEX
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1 is non zero complex set
(- 1) (#) r is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- r) " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (r ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) " is non zero complex set
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- 1 is non zero complex set
(- 1) (#) r is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq /" r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq (#) (r ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- (seq /" r) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) (#) (seq /" r) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) (#) seq is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- seq) /" r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- seq) (#) (r ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq /" (- r) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- r) " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq (#) ((- r) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1r) (#) (seq /" r) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((- 1r) (#) seq) (#) (r ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (r ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) ((- 1r) (#) (r ")) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) (r ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (seq (#) (r ")) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r /" seq) + (n /" seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r + n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r + n) /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r + n) (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r /" seq) - (n /" seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (n /" seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- 1 is non zero complex set
(- 1) (#) (n /" seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r /" seq) + (- (n /" seq)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r - n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r - n) /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r - n) (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r + n) (#) (seq ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r - n) (#) (seq ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n /" r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n (#) (r ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
seq1 (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(n /" r) + (seq1 /" seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 (#) r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(n (#) seq) + (seq1 (#) r) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((n (#) seq) + (seq1 (#) r)) /" (r (#) seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
((n (#) seq) + (seq1 (#) r)) (#) ((r (#) seq) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(n /" r) - (seq1 /" seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (seq1 /" seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
- 1 is non zero complex set
(- 1) (#) (seq1 /" seq) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(n /" r) + (- (seq1 /" seq)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(n (#) seq) - (seq1 (#) r) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- (seq1 (#) r) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) (seq1 (#) r) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(n (#) seq) + (- (seq1 (#) r)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
((n (#) seq) - (seq1 (#) r)) /" (r (#) seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((n (#) seq) - (seq1 (#) r)) (#) ((r (#) seq) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(n (#) seq) /" (r (#) seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(n (#) seq) (#) ((r (#) seq) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
((n (#) seq) /" (r (#) seq)) + (seq1 /" seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq1 (#) r) /" (r (#) seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq1 (#) r) (#) ((r (#) seq) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
((n (#) seq) /" (r (#) seq)) + ((seq1 (#) r) /" (r (#) seq)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq) " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((n (#) seq) + (seq1 (#) r)) (#) ((r (#) seq) ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((n (#) seq) /" (r (#) seq)) - (seq1 /" seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((n (#) seq) /" (r (#) seq)) + (- (seq1 /" seq)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
((n (#) seq) /" (r (#) seq)) - ((seq1 (#) r) /" (r (#) seq)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- ((seq1 (#) r) /" (r (#) seq)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(- 1) (#) ((seq1 (#) r) /" (r (#) seq)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
((n (#) seq) /" (r (#) seq)) + (- ((seq1 (#) r) /" (r (#) seq))) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
((n (#) seq) - (seq1 (#) r)) (#) ((r (#) seq) ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq (#) n is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n /" seq1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n (#) (seq1 ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r /" seq) /" (n /" seq1) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(n /" seq1) " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r /" seq) (#) ((n /" seq1) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) seq1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq1) /" (seq (#) n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq (#) n) " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(r (#) seq1) (#) ((seq (#) n) ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq1 ") " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(n ") (#) ((seq1 ") ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r /" seq) (#) ((n ") (#) ((seq1 ") ")) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) (seq ")) (#) seq1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((r (#) (seq ")) (#) seq1) (#) (n ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 (#) (seq ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq1 (#) (seq ")) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) (seq1 (#) (seq "))) (#) (n ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq1 (#) (seq ")) (#) (n ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) ((seq1 (#) (seq ")) (#) (n ")) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq ") (#) (n ") is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq1 (#) ((seq ") (#) (n ")) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) (seq1 (#) ((seq ") (#) (n "))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(r (#) seq1) (#) ((seq ") (#) (n ")) is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.r.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.(r (#) seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.r.| (#) |.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
|.(r (#) seq).| . n is complex V31() V32() Element of REAL
(r (#) seq) . n is complex Element of COMPLEX
|.((r (#) seq) . n).| is complex V31() V32() Element of REAL
r . n is complex Element of COMPLEX
seq . n is complex Element of COMPLEX
(r . n) * (seq . n) is complex Element of COMPLEX
|.((r . n) * (seq . n)).| is complex V31() V32() Element of REAL
|.(r . n).| is complex V31() V32() Element of REAL
|.(seq . n).| is complex V31() V32() Element of REAL
|.(r . n).| * |.(seq . n).| is complex set
|.r.| . n is complex V31() V32() Element of REAL
(|.r.| . n) * |.(seq . n).| is complex set
|.seq.| . n is complex V31() V32() Element of REAL
(|.r.| . n) * (|.seq.| . n) is complex set
(|.r.| (#) |.seq.|) . n is complex V31() V32() Element of REAL
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.r.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
r . seq is complex Element of COMPLEX
|.(r . seq).| is complex V31() V32() Element of REAL
|.r.| . seq is complex V31() V32() Element of REAL
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.r.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.r.| " is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.(r ").| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
|.(r ").| . seq is complex V31() V32() Element of REAL
(r ") . seq is complex Element of COMPLEX
|.((r ") . seq).| is complex V31() V32() Element of REAL
r . seq is complex Element of COMPLEX
(r . seq) " is complex Element of COMPLEX
|.((r . seq) ").| is complex V31() V32() Element of REAL
1r / (r . seq) is complex Element of COMPLEX
|.(1r / (r . seq)).| is complex V31() V32() Element of REAL
|.(r . seq).| is complex V31() V32() Element of REAL
1 / |.(r . seq).| is complex Element of COMPLEX
|.(r . seq).| " is complex set
|.r.| . seq is complex V31() V32() Element of REAL
(|.r.| . seq) " is complex set
(|.r.| ") . seq is complex V31() V32() Element of REAL
r is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.r.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r /" seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
r (#) (seq ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
|.(r /" seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.r.| /" |.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.seq.| " is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
|.r.| (#) (|.seq.| ") is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
seq " is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.(seq ").| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.r.| (#) |.(seq ").| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is complex Element of COMPLEX
|.r.| is complex V31() V32() Element of REAL
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
r (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.(r (#) seq).| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
|.r.| (#) |.seq.| is Relation-like NAT -defined REAL -valued Function-like non zero V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural complex V31() V32() V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT
|.(r (#) seq).| . n is complex V31() V32() Element of REAL
(r (#) seq) . n is complex Element of COMPLEX
|.((r (#) seq) . n).| is complex V31() V32() Element of REAL
seq . n is complex Element of COMPLEX
r * (seq . n) is complex Element of COMPLEX
|.(r * (seq . n)).| is complex V31() V32() Element of REAL
|.(seq . n).| is complex V31() V32() Element of REAL
|.r.| * |.(seq . n).| is complex set
|.seq.| . n is complex V31() V32() Element of REAL
|.r.| * (|.seq.| . n) is complex set
(|.r.| (#) |.seq.|) . n is complex V31() V32() Element of REAL