:: COMSEQ_3 semantic presentation

REAL is non zero V50() V62() V63() V64() V68() set

NAT is non zero epsilon-transitive epsilon-connected ordinal V62() V63() V64() V65() V66() V67() V68() Element of K19(REAL)

K19(REAL) is set

0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V62() V63() V64() V65() V66() V67() V68() set

1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

{0,1} is non zero V62() V63() V64() V65() V66() V67() set

INT is non zero V50() V62() V63() V64() V65() V66() V68() set

COMPLEX is non zero V50() V62() V68() set

omega is non zero epsilon-transitive epsilon-connected ordinal V62() V63() V64() V65() V66() V67() V68() set

K19(omega) is set

K19(NAT) is set

RAT is non zero V50() V62() V63() V64() V65() V68() set

K20(NAT,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(NAT,REAL)) is set

K20(COMPLEX,COMPLEX) is complex-valued set

K19(K20(COMPLEX,COMPLEX)) is set

K20(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(COMPLEX,REAL)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(REAL,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(REAL,REAL)) is set

K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K19(K20(K20(NAT,NAT),NAT)) is set

0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V48() V61() V62() V63() V64() V65() V66() V67() V68() Element of NAT

2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

1r is complex Element of COMPLEX

<i> is complex Element of COMPLEX

|.0.| is complex real ext-real V61() Element of REAL

|.1r.| is complex real ext-real Element of REAL

K20(NAT,COMPLEX) is complex-valued set

K19(K20(NAT,COMPLEX)) is set

K19(K20(NAT,NAT)) is set

0c is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V62() V63() V64() V65() V66() V67() V68() Element of COMPLEX

0 * <i> is complex set

0 + (0 * <i>) is complex set

C is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

C + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(D + 1) * <i> is complex set

C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

abs C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums (abs C) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

D is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(abs C) . D is complex real ext-real Element of REAL

(Partial_Sums (abs C)) . D is complex real ext-real Element of REAL

D + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(abs C) . (D + 1) is complex real ext-real Element of REAL

(Partial_Sums (abs C)) . (D + 1) is complex real ext-real Element of REAL

0 + ((abs C) . (D + 1)) is complex real ext-real Element of REAL

abs 0 is complex real ext-real V61() Element of REAL

(abs 0) + ((abs C) . (D + 1)) is complex real ext-real Element of REAL

C . D is complex real ext-real Element of REAL

abs (C . D) is complex real ext-real Element of REAL

(abs (C . D)) + ((abs C) . (D + 1)) is complex real ext-real Element of REAL

((Partial_Sums (abs C)) . D) + ((abs C) . (D + 1)) is complex real ext-real Element of REAL

D is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums (abs C)) . D is complex real ext-real Element of REAL

(abs C) . 0 is complex real ext-real Element of REAL

(Partial_Sums (abs C)) . 0 is complex real ext-real Element of REAL

(abs C) . D is complex real ext-real Element of REAL

C . D is complex real ext-real Element of REAL

abs (C . D) is complex real ext-real Element of REAL

abs 0 is complex real ext-real V61() Element of REAL

C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

abs C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums (abs C) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

D is complex real ext-real set

seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums (abs C)) . seq is complex real ext-real Element of REAL

((Partial_Sums (abs C)) . seq) - 0 is complex real ext-real Element of REAL

abs (((Partial_Sums (abs C)) . seq) - 0) is complex real ext-real Element of REAL

(Partial_Sums (abs C)) . seq is complex real ext-real Element of REAL

((Partial_Sums (abs C)) . seq) - 0 is complex real ext-real Element of REAL

abs (((Partial_Sums (abs C)) . seq) - 0) is complex real ext-real Element of REAL

0 - 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V62() V63() V64() V65() V66() V67() V68() Element of REAL

abs (0 - 0) is complex real ext-real Element of REAL

NAT --> 0 is Relation-like NAT -defined NAT -valued INT -valued RAT -valued Function-like constant non zero total V18( NAT , NAT ) T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,NAT))

C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

D is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

C . D is complex real ext-real Element of REAL

D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

seq is complex real ext-real Element of REAL

seq / 2 is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D . m is complex real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D . n is complex real ext-real Element of REAL

(D . n) - (D . m) is complex real ext-real Element of REAL

abs ((D . n) - (D . m)) is complex real ext-real Element of REAL

D . n is complex real ext-real Element of REAL

(D . n) - (D . m) is complex real ext-real Element of REAL

abs ((D . n) - (D . m)) is complex real ext-real Element of REAL

(seq / 2) + (seq / 2) is complex real ext-real Element of REAL

(abs ((D . n) - (D . m))) + (abs ((D . n) - (D . m))) is complex real ext-real Element of REAL

(D . n) - (D . n) is complex real ext-real Element of REAL

abs ((D . n) - (D . n)) is complex real ext-real Element of REAL

((D . n) - (D . m)) - ((D . n) - (D . m)) is complex real ext-real Element of REAL

abs (((D . n) - (D . m)) - ((D . n) - (D . m))) is complex real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D . n is complex real ext-real Element of REAL

D . n is complex real ext-real Element of REAL

(D . n) - (D . n) is complex real ext-real Element of REAL

abs ((D . n) - (D . n)) is complex real ext-real Element of REAL

D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

seq is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . m is complex real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

m + n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . (m + n) is complex real ext-real Element of REAL

((Partial_Sums D) . (m + n)) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL

seq * n is complex real ext-real Element of REAL

(m + n) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D . ((m + n) + 1) is complex real ext-real Element of REAL

(seq * n) + (D . ((m + n) + 1)) is complex real ext-real Element of REAL

(seq * n) + seq is complex real ext-real Element of REAL

n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

m + (n + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . (m + (n + 1)) is complex real ext-real Element of REAL

((Partial_Sums D) . (m + (n + 1))) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL

((Partial_Sums D) . (m + n)) + (D . ((m + n) + 1)) is complex real ext-real Element of REAL

(((Partial_Sums D) . (m + n)) + (D . ((m + n) + 1))) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL

(((Partial_Sums D) . (m + n)) - ((Partial_Sums D) . m)) + (D . ((m + n) + 1)) is complex real ext-real Element of REAL

seq * (n + 1) is complex real ext-real Element of REAL

m + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . (m + 0) is complex real ext-real Element of REAL

((Partial_Sums D) . (m + 0)) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL

seq * 0 is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

m + n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . (m + n) is complex real ext-real Element of REAL

(Partial_Sums D) . m is complex real ext-real Element of REAL

((Partial_Sums D) . (m + n)) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL

seq * n is complex real ext-real Element of REAL

D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

seq is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . m is complex real ext-real Element of REAL

m + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

seq * (m + 1) is complex real ext-real Element of REAL

D . (m + 1) is complex real ext-real Element of REAL

(seq * (m + 1)) + (D . (m + 1)) is complex real ext-real Element of REAL

(seq * (m + 1)) + seq is complex real ext-real Element of REAL

(Partial_Sums D) . (m + 1) is complex real ext-real Element of REAL

((Partial_Sums D) . m) + (D . (m + 1)) is complex real ext-real Element of REAL

(m + 1) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

seq * ((m + 1) + 1) is complex real ext-real Element of REAL

(Partial_Sums D) . 0 is complex real ext-real Element of REAL

D . 0 is complex real ext-real Element of REAL

0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

seq * (0 + 1) is complex real ext-real Element of REAL

D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total 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 total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . m is complex real ext-real Element of REAL

(Partial_Sums seq) . m is complex real ext-real Element of REAL

n is complex real ext-real Element of REAL

n * ((Partial_Sums seq) . m) is complex real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . n is complex real ext-real Element of REAL

(Partial_Sums seq) . n is complex real ext-real Element of REAL

n * ((Partial_Sums seq) . n) is complex real ext-real Element of REAL

n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D . (n + 1) is complex real ext-real Element of REAL

seq . (n + 1) is complex real ext-real Element of REAL

n * (seq . (n + 1)) is complex real ext-real Element of REAL

(n * ((Partial_Sums seq) . n)) + (D . (n + 1)) is complex real ext-real Element of REAL

(n * ((Partial_Sums seq) . n)) + (n * (seq . (n + 1))) is complex real ext-real Element of REAL

(Partial_Sums D) . (n + 1) is complex real ext-real Element of REAL

((Partial_Sums D) . n) + (D . (n + 1)) is complex real ext-real Element of REAL

((Partial_Sums seq) . n) + (seq . (n + 1)) is complex real ext-real Element of REAL

n * (((Partial_Sums seq) . n) + (seq . (n + 1))) is complex real ext-real Element of REAL

(Partial_Sums seq) . (n + 1) is complex real ext-real Element of REAL

n * ((Partial_Sums seq) . (n + 1)) is complex real ext-real Element of REAL

(Partial_Sums D) . 0 is complex real ext-real Element of REAL

(Partial_Sums seq) . 0 is complex real ext-real Element of REAL

n * ((Partial_Sums seq) . 0) is complex real ext-real Element of REAL

D . 0 is complex real ext-real Element of REAL

seq . 0 is complex real ext-real Element of REAL

n * (seq . 0) is complex real ext-real Element of REAL

D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total 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 total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

n is complex real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . n is complex real ext-real Element of REAL

(Partial_Sums seq) . n is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

n + m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . (n + m) is complex real ext-real Element of REAL

((Partial_Sums D) . (n + m)) - ((Partial_Sums D) . n) is complex real ext-real Element of REAL

(Partial_Sums seq) . (n + m) is complex real ext-real Element of REAL

((Partial_Sums seq) . (n + m)) - ((Partial_Sums seq) . n) is complex real ext-real Element of REAL

n * (((Partial_Sums seq) . (n + m)) - ((Partial_Sums seq) . n)) is complex real ext-real Element of REAL

m + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

n + (m + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . (n + (m + 1)) is complex real ext-real Element of REAL

((Partial_Sums D) . (n + (m + 1))) - ((Partial_Sums D) . n) is complex real ext-real Element of REAL

(Partial_Sums seq) . (n + (m + 1)) is complex real ext-real Element of REAL

((Partial_Sums seq) . (n + (m + 1))) - ((Partial_Sums seq) . n) is complex real ext-real Element of REAL

n * (((Partial_Sums seq) . (n + (m + 1))) - ((Partial_Sums seq) . n)) is complex real ext-real Element of REAL

(n + m) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D . ((n + m) + 1) is complex real ext-real Element of REAL

((Partial_Sums D) . (n + m)) + (D . ((n + m) + 1)) is complex real ext-real Element of REAL

seq . ((n + m) + 1) is complex real ext-real Element of REAL

n * (seq . ((n + m) + 1)) is complex real ext-real Element of REAL

((Partial_Sums D) . (n + m)) + (n * (seq . ((n + m) + 1))) is complex real ext-real Element of REAL

(((Partial_Sums D) . (n + m)) + (n * (seq . ((n + m) + 1)))) - ((Partial_Sums D) . n) is complex real ext-real Element of REAL

(((Partial_Sums D) . (n + m)) - ((Partial_Sums D) . n)) + (n * (seq . ((n + m) + 1))) is complex real ext-real Element of REAL

(n * (((Partial_Sums seq) . (n + m)) - ((Partial_Sums seq) . n))) + (n * (seq . ((n + m) + 1))) is complex real ext-real Element of REAL

((Partial_Sums seq) . (n + m)) + (seq . ((n + m) + 1)) is complex real ext-real Element of REAL

(((Partial_Sums seq) . (n + m)) + (seq . ((n + m) + 1))) - ((Partial_Sums seq) . n) is complex real ext-real Element of REAL

n * ((((Partial_Sums seq) . (n + m)) + (seq . ((n + m) + 1))) - ((Partial_Sums seq) . n)) is complex real ext-real Element of REAL

n + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . (n + 0) is complex real ext-real Element of REAL

((Partial_Sums D) . (n + 0)) - ((Partial_Sums D) . n) is complex real ext-real Element of REAL

(Partial_Sums seq) . (n + 0) is complex real ext-real Element of REAL

((Partial_Sums seq) . (n + 0)) - ((Partial_Sums seq) . n) is complex real ext-real Element of REAL

n * (((Partial_Sums seq) . (n + 0)) - ((Partial_Sums seq) . n)) is complex real ext-real Element of REAL

D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total 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 real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . seq is complex real ext-real Element of REAL

(Partial_Sums D) . m is complex real ext-real Element of REAL

((Partial_Sums D) . seq) - ((Partial_Sums D) . seq) is complex real ext-real Element of REAL

((Partial_Sums D) . m) - ((Partial_Sums D) . seq) is complex real ext-real Element of REAL

abs (((Partial_Sums D) . m) - ((Partial_Sums D) . seq)) is complex real ext-real Element of REAL

(Partial_Sums D) . 0 is complex real ext-real Element of REAL

seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . seq is complex real ext-real Element of REAL

D . 0 is complex real ext-real Element of REAL

abs ((Partial_Sums D) . seq) is complex real ext-real Element of REAL

seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . m is complex real ext-real Element of REAL

(Partial_Sums D) . seq is complex real ext-real Element of REAL

((Partial_Sums D) . m) - ((Partial_Sums D) . seq) is complex real ext-real Element of REAL

abs (((Partial_Sums D) . m) - ((Partial_Sums D) . seq)) is complex real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(Partial_Sums D) . n is complex real ext-real Element of REAL

abs ((Partial_Sums D) . n) is complex real ext-real Element of REAL

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

lim D is complex Element of COMPLEX

seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

D - seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

- seq is Relation-like NAT -defined Function-like total complex-valued set

- 1 is non zero complex real ext-real non positive negative set

(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued set

D + (- seq) is Relation-like NAT -defined Function-like total complex-valued set

lim (D - seq) is complex Element of COMPLEX

lim seq is complex Element of COMPLEX

(lim D) - (lim seq) is complex Element of COMPLEX

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

|.D.| is Relation-like NAT -defined REAL -valued Function-like non zero total 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 real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D . seq is complex Element of COMPLEX

|.(D . seq).| is complex real ext-real Element of REAL

|.D.| . seq is complex real ext-real Element of REAL

D is complex set

seq is complex Element of COMPLEX

m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

m . 0 is complex Element of COMPLEX

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

m . (n + 1) is complex Element of COMPLEX

m . n is complex Element of COMPLEX

(m . n) * D is complex set

seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

seq . 0 is complex Element of COMPLEX

m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

m . 0 is complex Element of COMPLEX

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

seq . n is complex Element of COMPLEX

m . n is complex Element of COMPLEX

n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

seq . (n + 1) is complex Element of COMPLEX

m . (n + 1) is complex Element of COMPLEX

(m . n) * D is complex set

D is complex set

seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set

D |^ seq is complex set

(D) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) . seq is complex Element of COMPLEX

n is complex Element of COMPLEX

n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D |^ n is complex set

(D) . n is complex Element of COMPLEX

n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D |^ (n + 1) is complex set

(D) . (n + 1) is complex Element of COMPLEX

((D) . n) * D is complex set

D |^ 0 is complex set

(D) . 0 is complex Element of COMPLEX

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D |^ m is complex set

(D) . m is complex Element of COMPLEX

D is complex Element of COMPLEX

(D,0) is complex Element of COMPLEX

(D) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) . 0 is complex Element of COMPLEX

D is Relation-like Function-like complex-valued set

dom D is set

m is Relation-like Function-like set

dom m is set

m is Relation-like Function-like set

dom m is set

n is Relation-like Function-like set

dom n is set

n is set

m . n is set

D . n is complex set

Re (D . n) is complex real ext-real Element of REAL

n . n is set

m is Relation-like Function-like set

dom m is set

m is Relation-like Function-like set

dom m is set

n is Relation-like Function-like set

dom n is set

n is set

m . n is set

D . n is complex set

Im (D . n) is complex real ext-real Element of REAL

n . n is set

D is Relation-like Function-like complex-valued set

(D) is Relation-like Function-like set

seq is set

dom (D) is set

(D) . seq is set

D . seq is complex set

Re (D . seq) is complex real ext-real Element of REAL

(D) is Relation-like Function-like set

seq is set

dom (D) is set

(D) . seq is set

D . seq is complex set

Im (D . seq) is complex real ext-real Element of REAL

D is set

K20(D,COMPLEX) is complex-valued set

K19(K20(D,COMPLEX)) is set

seq is Relation-like D -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(D,COMPLEX))

(seq) is Relation-like Function-like complex-valued ext-real-valued real-valued set

K20(D,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(D,REAL)) is set

dom seq is set

rng (seq) is V62() V63() V64() set

dom (seq) is set

(seq) is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom seq is set

rng (seq) is V62() V63() V64() set

dom (seq) is set

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) is Relation-like Function-like complex-valued ext-real-valued real-valued set

(NAT,D) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

dom (NAT,D) is V62() V63() V64() V65() V66() V67() set

dom D is V62() V63() V64() V65() V66() V67() set

seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(NAT,D) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

dom (NAT,D) is V62() V63() V64() V65() V66() V67() set

dom D is V62() V63() V64() V65() V66() V67() set

dom seq is V62() V63() V64() V65() V66() V67() set

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

seq . m is complex real ext-real Element of REAL

D . m is complex Element of COMPLEX

Re (D . m) is complex real ext-real Element of REAL

m is set

seq . m is complex real ext-real Element of REAL

D . m is complex set

Re (D . m) is complex real ext-real Element of REAL

(NAT,D) . m is complex real ext-real Element of REAL

(D) is Relation-like Function-like complex-valued ext-real-valued real-valued set

(NAT,D) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

dom (NAT,D) is V62() V63() V64() V65() V66() V67() set

dom D is V62() V63() V64() V65() V66() V67() set

seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(NAT,D) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

dom (NAT,D) is V62() V63() V64() V65() V66() V67() set

dom D is V62() V63() V64() V65() V66() V67() set

dom seq is V62() V63() V64() V65() V66() V67() set

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

seq . m is complex real ext-real Element of REAL

D . m is complex Element of COMPLEX

Im (D . m) is complex real ext-real Element of REAL

m is set

seq . m is complex real ext-real Element of REAL

D . m is complex set

Im (D . m) is complex real ext-real Element of REAL

(NAT,D) . m is complex real ext-real Element of REAL

D is complex Element of COMPLEX

|.D.| is complex real ext-real Element of REAL

Re D is complex real ext-real Element of REAL

abs (Re D) is complex real ext-real Element of REAL

Im D is complex real ext-real Element of REAL

abs (Im D) is complex real ext-real Element of REAL

(abs (Re D)) + (abs (Im D)) is complex real ext-real Element of REAL

(Im D) * <i> is complex set

(Re D) + ((Im D) * <i>) is complex set

(Re D) + (0 * <i>) is complex set

|.((Re D) + (0 * <i>)).| is complex real ext-real Element of REAL

0 + ((Im D) * <i>) is complex set

|.(0 + ((Im D) * <i>)).| is complex real ext-real Element of REAL

|.((Re D) + (0 * <i>)).| + |.(0 + ((Im D) * <i>)).| is complex real ext-real Element of REAL

Re (0 + ((Im D) * <i>)) is complex real ext-real Element of REAL

Im (0 + ((Im D) * <i>)) is complex real ext-real Element of REAL

D is complex Element of COMPLEX

Re D is complex real ext-real Element of REAL

abs (Re D) is complex real ext-real Element of REAL

|.D.| is complex real ext-real Element of REAL

Im D is complex real ext-real Element of REAL

abs (Im D) is complex real ext-real Element of REAL

(Re D) ^2 is complex real ext-real Element of REAL

(Re D) * (Re D) is complex real ext-real set

(Im D) ^2 is complex real ext-real Element of REAL

(Im D) * (Im D) is complex real ext-real set

0 + ((Im D) ^2) is complex real ext-real Element of REAL

((Re D) ^2) + ((Im D) ^2) is complex real ext-real Element of REAL

sqrt ((Im D) ^2) is complex real ext-real Element of REAL

sqrt (((Re D) ^2) + ((Im D) ^2)) is complex real ext-real Element of REAL

0 + ((Re D) ^2) is complex real ext-real Element of REAL

((Im D) ^2) + ((Re D) ^2) is complex real ext-real Element of REAL

sqrt ((Re D) ^2) is complex real ext-real Element of REAL

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total 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 total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total 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 total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

D . m is complex Element of COMPLEX

Im (D . m) is complex real ext-real Element of REAL

(seq) . m is complex real ext-real Element of REAL

seq . m is complex Element of COMPLEX

Im (seq . m) is complex real ext-real Element of REAL

Re (D . m) is complex real ext-real Element of REAL

(seq) . m is complex real ext-real Element of REAL

Re (seq . m) is complex real ext-real Element of REAL

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total 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 total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) + (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

D + seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

((D + seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total 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 total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) + (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((D + seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

((D) + (seq)) . m is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

(seq) . m is complex real ext-real Element of REAL

((D) . m) + ((seq) . m) is complex real ext-real Element of REAL

D . m is complex Element of COMPLEX

Re (D . m) is complex real ext-real Element of REAL

(Re (D . m)) + ((seq) . m) is complex real ext-real Element of REAL

seq . m is complex Element of COMPLEX

Re (seq . m) is complex real ext-real Element of REAL

(Re (D . m)) + (Re (seq . m)) is complex real ext-real Element of REAL

(D . m) + (seq . m) is complex Element of COMPLEX

Re ((D . m) + (seq . m)) is complex real ext-real Element of REAL

(D + seq) . m is complex Element of COMPLEX

Re ((D + seq) . m) is complex real ext-real Element of REAL

((D + seq)) . m is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

((D) + (seq)) . m is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

(seq) . m is complex real ext-real Element of REAL

((D) . m) + ((seq) . m) is complex real ext-real Element of REAL

D . m is complex Element of COMPLEX

Im (D . m) is complex real ext-real Element of REAL

(Im (D . m)) + ((seq) . m) is complex real ext-real Element of REAL

seq . m is complex Element of COMPLEX

Im (seq . m) is complex real ext-real Element of REAL

(Im (D . m)) + (Im (seq . m)) is complex real ext-real Element of REAL

(D . m) + (seq . m) is complex Element of COMPLEX

Im ((D . m) + (seq . m)) is complex real ext-real Element of REAL

(D + seq) . m is complex Element of COMPLEX

Im ((D + seq) . m) is complex real ext-real Element of REAL

((D + seq)) . m is complex real ext-real Element of REAL

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- 1 is non zero complex real ext-real non positive negative set

(- 1) (#) (D) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

- D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(- 1) (#) D is Relation-like NAT -defined Function-like total complex-valued set

((- D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(- 1) (#) (D) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

((- D)) is Relation-like NAT -defined REAL -valued Function-like non zero total 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 real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(- (D)) . seq is complex real ext-real Element of REAL

(D) . seq is complex real ext-real Element of REAL

- ((D) . seq) is complex real ext-real Element of REAL

D . seq is complex Element of COMPLEX

Re (D . seq) is complex real ext-real Element of REAL

- (Re (D . seq)) is complex real ext-real Element of REAL

- (D . seq) is complex Element of COMPLEX

Re (- (D . seq)) is complex real ext-real Element of REAL

(- D) . seq is complex Element of COMPLEX

Re ((- D) . seq) is complex real ext-real Element of REAL

((- D)) . seq is complex real ext-real Element of REAL

seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(- (D)) . seq is complex real ext-real Element of REAL

(D) . seq is complex real ext-real Element of REAL

- ((D) . seq) is complex real ext-real Element of REAL

D . seq is complex Element of COMPLEX

Im (D . seq) is complex real ext-real Element of REAL

- (Im (D . seq)) is complex real ext-real Element of REAL

- (D . seq) is complex Element of COMPLEX

Im (- (D . seq)) is complex real ext-real Element of REAL

(- D) . seq is complex Element of COMPLEX

Im ((- D) . seq) is complex real ext-real Element of REAL

((- D)) . seq is complex real ext-real Element of REAL

D is complex real ext-real Element of REAL

seq is complex Element of COMPLEX

Re seq is complex real ext-real Element of REAL

D * (Re seq) is complex real ext-real Element of REAL

D * seq is complex set

Re (D * seq) is complex real ext-real Element of REAL

Im seq is complex real ext-real Element of REAL

D * (Im seq) is complex real ext-real Element of REAL

Im (D * seq) is complex real ext-real Element of REAL

D + (0 * <i>) is complex set

Re D is complex real ext-real Element of REAL

Im D is complex real ext-real Element of REAL

m is complex Element of COMPLEX

Re m is complex real ext-real Element of REAL

(Re m) * (Re seq) is complex real ext-real Element of REAL

Im m is complex real ext-real Element of REAL

(Im m) * (Im seq) is complex real ext-real Element of REAL

((Re m) * (Re seq)) - ((Im m) * (Im seq)) is complex real ext-real Element of REAL

(Re m) * (Im seq) is complex real ext-real Element of REAL

(Re seq) * (Im m) is complex real ext-real Element of REAL

((Re m) * (Im seq)) + ((Re seq) * (Im m)) is complex real ext-real Element of REAL

(((Re m) * (Im seq)) + ((Re seq) * (Im m))) * <i> is complex set

(((Re m) * (Re seq)) - ((Im m) * (Im seq))) + ((((Re m) * (Im seq)) + ((Re seq) * (Im m))) * <i>) is complex set

(D * (Im seq)) * <i> is complex set

(D * (Re seq)) + ((D * (Im seq)) * <i>) is complex set

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total 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 total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) - (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- (seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

- 1 is non zero complex real ext-real non positive negative set

(- 1) (#) (seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

(D) + (- (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

D - seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

- seq is Relation-like NAT -defined Function-like total complex-valued set

(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued set

D + (- seq) is Relation-like NAT -defined Function-like total complex-valued set

((D - seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total 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 total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) - (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- (seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

(- 1) (#) (seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

(D) + (- (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

((D - seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

((D) - (seq)) . m is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

- (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(- (seq)) . m is complex real ext-real Element of REAL

((D) . m) + ((- (seq)) . m) is complex real ext-real Element of REAL

- seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

((- seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((- seq)) . m is complex real ext-real Element of REAL

((D) . m) + (((- seq)) . m) is complex real ext-real Element of REAL

(D) + ((- seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((D) + ((- seq))) . m is complex real ext-real Element of REAL

((D - seq)) . m is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

((D) - (seq)) . m is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

- (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(- (seq)) . m is complex real ext-real Element of REAL

((D) . m) + ((- (seq)) . m) is complex real ext-real Element of REAL

((- seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((- seq)) . m is complex real ext-real Element of REAL

((D) . m) + (((- seq)) . m) is complex real ext-real Element of REAL

(D) + ((- seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((D) + ((- seq))) . m is complex real ext-real Element of REAL

((D - seq)) . m is complex real ext-real Element of REAL

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

seq is complex real ext-real Element of REAL

seq (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

seq (#) D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

((seq (#) D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

seq (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((seq (#) D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(seq (#) (D)) . m is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

seq * ((D) . m) is complex real ext-real Element of REAL

D . m is complex Element of COMPLEX

Re (D . m) is complex real ext-real Element of REAL

seq * (Re (D . m)) is complex real ext-real Element of REAL

seq * (D . m) is complex set

Re (seq * (D . m)) is complex real ext-real Element of REAL

(seq (#) D) . m is complex Element of COMPLEX

Re ((seq (#) D) . m) is complex real ext-real Element of REAL

((seq (#) D)) . m is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

(seq (#) (D)) . m is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

seq * ((D) . m) is complex real ext-real Element of REAL

D . m is complex Element of COMPLEX

Im (D . m) is complex real ext-real Element of REAL

seq * (Im (D . m)) is complex real ext-real Element of REAL

seq * (D . m) is complex set

Im (seq * (D . m)) is complex real ext-real Element of REAL

(seq (#) D) . m is complex Element of COMPLEX

Im ((seq (#) D) . m) is complex real ext-real Element of REAL

((seq (#) D)) . m is complex real ext-real Element of REAL

D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

seq is complex Element of COMPLEX

seq (#) D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))

((seq (#) D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Re seq is complex real ext-real Element of REAL

(Re seq) (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Im seq is complex real ext-real Element of REAL

(Im seq) (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((Re seq) (#) (D)) - ((Im seq) (#) (D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- ((Im seq) (#) (D)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

- 1 is non zero complex real ext-real non positive negative set

(- 1) (#) ((Im seq) (#) (D)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

((Re seq) (#) (D)) + (- ((Im seq) (#) (D))) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set

((seq (#) D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(Re seq) (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(Im seq) (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((Re seq) (#) (D)) + ((Im seq) (#) (D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

((seq (#) D)) . m is complex real ext-real Element of REAL

(seq (#) D) . m is complex Element of COMPLEX

Re ((seq (#) D) . m) is complex real ext-real Element of REAL

D . m is complex Element of COMPLEX

seq * (D . m) is complex Element of COMPLEX

Re (seq * (D . m)) is complex real ext-real Element of REAL

Re (D . m) is complex real ext-real Element of REAL

(Re seq) * (Re (D . m)) is complex real ext-real Element of REAL

Im (D . m) is complex real ext-real Element of REAL

(Im seq) * (Im (D . m)) is complex real ext-real Element of REAL

((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m))) is complex real ext-real Element of REAL

(Re seq) * (Im (D . m)) is complex real ext-real Element of REAL

(Re (D . m)) * (Im seq) is complex real ext-real Element of REAL

((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq)) is complex real ext-real Element of REAL

(((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i> is complex set

(((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m)))) + ((((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i>) is complex set

Re ((((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m)))) + ((((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i>)) is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

(Re seq) * ((D) . m) is complex real ext-real Element of REAL

((Re seq) * ((D) . m)) - ((Im seq) * (Im (D . m))) is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

(Im seq) * ((D) . m) is complex real ext-real Element of REAL

((Re seq) * ((D) . m)) - ((Im seq) * ((D) . m)) is complex real ext-real Element of REAL

((Re seq) (#) (D)) . m is complex real ext-real Element of REAL

(((Re seq) (#) (D)) . m) - ((Im seq) * ((D) . m)) is complex real ext-real Element of REAL

((Im seq) (#) (D)) . m is complex real ext-real Element of REAL

(((Re seq) (#) (D)) . m) - (((Im seq) (#) (D)) . m) is complex real ext-real Element of REAL

- (((Im seq) (#) (D)) . m) is complex real ext-real Element of REAL

(((Re seq) (#) (D)) . m) + (- (((Im seq) (#) (D)) . m)) is complex real ext-real Element of REAL

- ((Im seq) (#) (D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(- ((Im seq) (#) (D))) . m is complex real ext-real Element of REAL

(((Re seq) (#) (D)) . m) + ((- ((Im seq) (#) (D))) . m) is complex real ext-real Element of REAL

(((Re seq) (#) (D)) - ((Im seq) (#) (D))) . m is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT

((seq (#) D)) . m is complex real ext-real Element of REAL

(seq (#) D) . m is complex Element of COMPLEX

Im ((seq (#) D) . m) is complex real ext-real Element of REAL

D . m is complex Element of COMPLEX

seq * (D . m) is complex Element of COMPLEX

Im (seq * (D . m)) is complex real ext-real Element of REAL

Re (D . m) is complex real ext-real Element of REAL

(Re seq) * (Re (D . m)) is complex real ext-real Element of REAL

Im (D . m) is complex real ext-real Element of REAL

(Im seq) * (Im (D . m)) is complex real ext-real Element of REAL

((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m))) is complex real ext-real Element of REAL

(Re seq) * (Im (D . m)) is complex real ext-real Element of REAL

(Re (D . m)) * (Im seq) is complex real ext-real Element of REAL

((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq)) is complex real ext-real Element of REAL

(((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i> is complex set

(((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m)))) + ((((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i>) is complex set

Im ((((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m)))) + ((((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i>)) is complex real ext-real Element of REAL

(D) . m is complex real ext-real Element of REAL

(Im seq) * ((D) . m) is complex real ext-real Element of REAL

((Re seq) * (Im (D . m))) + ((Im seq) * ((D) . m)) is complex