:: LOPBAN_4 semantic presentation

REAL is V1() V47() V59() V60() V61() V65() set
NAT is V1() epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V47() V59() V65() set
omega is V1() epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() set
K6(omega) is set
K6(NAT) is set
RAT is V1() V47() V59() V60() V61() V62() V65() set
INT is V1() V47() V59() V60() V61() V62() V63() V65() set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is complex-valued set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
K380() is V1() set
K7(K380(),K380()) is set
K7(K7(K380(),K380()),K380()) is set
K6(K7(K7(K380(),K380()),K380())) is set
K7(REAL,K380()) is set
K7(K7(REAL,K380()),K380()) is set
K6(K7(K7(REAL,K380()),K380())) is set
K386() is L12()
the carrier of K386() is set
K6( the carrier of K386()) is set
K390() is Element of K6( the carrier of K386())
K7(K390(),K390()) is set
K7(K7(K390(),K390()),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(K390(),K390()),REAL)) is set
the_set_of_l1RealSequences is Element of K6( the carrier of K386())
K7(the_set_of_l1RealSequences,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(the_set_of_l1RealSequences,REAL)) is set
0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() set
1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
Prod_real_n is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
0 ! is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive Element of REAL
4 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X is non empty multMagma
the carrier of X is V1() set
t is Element of the carrier of X
t * t is Element of the carrier of X
t is Element of the carrier of X
k is Element of the carrier of X
t * k is Element of the carrier of X
k * t is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z #N s is Element of the carrier of X
z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
(z GeoSeq) . s is Element of the carrier of X
z * (z #N s) is Element of the carrier of X
s + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z #N (s + 1) is Element of the carrier of X
(z GeoSeq) . (s + 1) is Element of the carrier of X
(z #N s) * z is Element of the carrier of X
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z #N (0 + 1) is Element of the carrier of X
(z GeoSeq) . (0 + 1) is Element of the carrier of X
(z GeoSeq) . 0 is Element of the carrier of X
((z GeoSeq) . 0) * z is Element of the carrier of X
1. X is Element of the carrier of X
(1. X) * z is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z #N t is Element of the carrier of X
(z GeoSeq) . t is Element of the carrier of X
z * (z #N t) is Element of the carrier of X
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z #N (t + 1) is Element of the carrier of X
(z GeoSeq) . (t + 1) is Element of the carrier of X
z * (z #N (t + 1)) is Element of the carrier of X
(t + 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z #N ((t + 1) + 1) is Element of the carrier of X
(z GeoSeq) . ((t + 1) + 1) is Element of the carrier of X
(z GeoSeq) . t is Element of the carrier of X
((z GeoSeq) . t) * z is Element of the carrier of X
z * (((z GeoSeq) . t) * z) is Element of the carrier of X
(z * (z #N t)) * z is Element of the carrier of X
z #N 0 is Element of the carrier of X
(z GeoSeq) . 0 is Element of the carrier of X
z * (z #N 0) is Element of the carrier of X
z * (1. X) is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z #N t is Element of the carrier of X
(z GeoSeq) . t is Element of the carrier of X
z * (z #N t) is Element of the carrier of X
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z #N (t + 1) is Element of the carrier of X
(z GeoSeq) . (t + 1) is Element of the carrier of X
(z #N t) * z is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of X
s #N z is Element of the carrier of X
s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
(s GeoSeq) . z is Element of the carrier of X
t is Element of the carrier of X
t * (s #N z) is Element of the carrier of X
(s #N z) * t is Element of the carrier of X
t #N z is Element of the carrier of X
t GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(t GeoSeq) . z is Element of the carrier of X
s * (t #N z) is Element of the carrier of X
(t #N z) * s is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s #N k is Element of the carrier of X
(s GeoSeq) . k is Element of the carrier of X
t * (s #N k) is Element of the carrier of X
(s #N k) * t is Element of the carrier of X
t #N k is Element of the carrier of X
(t GeoSeq) . k is Element of the carrier of X
s * (t #N k) is Element of the carrier of X
(t #N k) * s is Element of the carrier of X
k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s #N (k + 1) is Element of the carrier of X
(s GeoSeq) . (k + 1) is Element of the carrier of X
t * (s #N (k + 1)) is Element of the carrier of X
(s #N (k + 1)) * t is Element of the carrier of X
t #N (k + 1) is Element of the carrier of X
(t GeoSeq) . (k + 1) is Element of the carrier of X
s * (t #N (k + 1)) is Element of the carrier of X
(t #N (k + 1)) * s is Element of the carrier of X
(t #N k) * t is Element of the carrier of X
s * ((t #N k) * t) is Element of the carrier of X
(s * (t #N k)) * t is Element of the carrier of X
s * t is Element of the carrier of X
(t #N k) * (s * t) is Element of the carrier of X
t * s is Element of the carrier of X
(t #N k) * (t * s) is Element of the carrier of X
((t #N k) * t) * s is Element of the carrier of X
(s #N k) * s is Element of the carrier of X
t * ((s #N k) * s) is Element of the carrier of X
(t * (s #N k)) * s is Element of the carrier of X
(s #N k) * (t * s) is Element of the carrier of X
(s #N k) * (s * t) is Element of the carrier of X
((s #N k) * s) * t is Element of the carrier of X
t #N 0 is Element of the carrier of X
(t GeoSeq) . 0 is Element of the carrier of X
1. X is Element of the carrier of X
s * (t #N 0) is Element of the carrier of X
(t #N 0) * s is Element of the carrier of X
s #N 0 is Element of the carrier of X
(s GeoSeq) . 0 is Element of the carrier of X
t * (s #N 0) is Element of the carrier of X
(s #N 0) * t is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
0. X is V82(X) Element of the carrier of X
z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim z is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
z - s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (z - s) is Element of the carrier of X
lim s is Element of the carrier of X
(lim z) - (lim s) is Element of the carrier of X
((lim z) - (lim s)) + (lim s) is Element of the carrier of X
(lim s) - (lim s) is Element of the carrier of X
(lim z) - ((lim s) - (lim s)) is Element of the carrier of X
(lim z) - (0. X) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim z is Element of the carrier of X
s is Element of the carrier of X
t is V11() real ext-real Element of REAL
k is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z . p is Element of the carrier of X
(z . p) - s is Element of the carrier of X
||.((z . p) - s).|| is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
t is Element of the carrier of X
||.z.|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is V11() real ext-real set
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z . p is Element of the carrier of X
||.(z . p).|| is V11() real ext-real Element of REAL
||.z.|| . p is V11() real ext-real Element of REAL
z . 1 is Element of the carrier of X
||.(z . 1).|| is V11() real ext-real Element of REAL
||.z.|| . 1 is V11() real ext-real Element of REAL
p is Element of the carrier of X
t * p is Element of the carrier of X
n is Element of the carrier of X
n is V11() real ext-real Element of REAL
||.p.|| is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
||.p.|| + k is V11() real ext-real Element of REAL
0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
n / (||.p.|| + k) is V11() real ext-real Element of REAL
n4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n4 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(z * s) . l is Element of the carrier of X
((z * s) . l) - n is Element of the carrier of X
||.(((z * s) . l) - n).|| is V11() real ext-real Element of REAL
s . l is Element of the carrier of X
(s . l) - p is Element of the carrier of X
||.((s . l) - p).|| is V11() real ext-real Element of REAL
z . l is Element of the carrier of X
||.(z . l).|| is V11() real ext-real Element of REAL
(z . l) * ((s . l) - p) is Element of the carrier of X
||.((z . l) * ((s . l) - p)).|| is V11() real ext-real Element of REAL
||.(z . l).|| * ||.((s . l) - p).|| is V11() real ext-real Element of REAL
(z . l) - t is Element of the carrier of X
||.((z . l) - t).|| is V11() real ext-real Element of REAL
(z * s) . l is Element of the carrier of X
((z * s) . l) - n is Element of the carrier of X
||.(((z * s) . l) - n).|| is V11() real ext-real Element of REAL
(z . l) * (s . l) is Element of the carrier of X
((z . l) * (s . l)) - (t * p) is Element of the carrier of X
||.(((z . l) * (s . l)) - (t * p)).|| is V11() real ext-real Element of REAL
(z . l) * p is Element of the carrier of X
((z . l) * (s . l)) - ((z . l) * p) is Element of the carrier of X
((z . l) * p) - (t * p) is Element of the carrier of X
(((z . l) * (s . l)) - ((z . l) * p)) + (((z . l) * p) - (t * p)) is Element of the carrier of X
||.((((z . l) * (s . l)) - ((z . l) * p)) + (((z . l) * p) - (t * p))).|| is V11() real ext-real Element of REAL
((z . l) * ((s . l) - p)) + (((z . l) * p) - (t * p)) is Element of the carrier of X
||.(((z . l) * ((s . l) - p)) + (((z . l) * p) - (t * p))).|| is V11() real ext-real Element of REAL
((z . l) - t) * p is Element of the carrier of X
((z . l) * ((s . l) - p)) + (((z . l) - t) * p) is Element of the carrier of X
||.(((z . l) * ((s . l) - p)) + (((z . l) - t) * p)).|| is V11() real ext-real Element of REAL
||.(((z . l) - t) * p).|| is V11() real ext-real Element of REAL
||.((z . l) * ((s . l) - p)).|| + ||.(((z . l) - t) * p).|| is V11() real ext-real Element of REAL
k * (n / (||.p.|| + k)) is V11() real ext-real Element of REAL
||.p.|| * ||.((z . l) - t).|| is V11() real ext-real Element of REAL
||.p.|| * (n / (||.p.|| + k)) is V11() real ext-real Element of REAL
(k * (n / (||.p.|| + k))) + (||.p.|| * (n / (||.p.|| + k))) is V11() real ext-real Element of REAL
(n / (||.p.|| + k)) * (||.p.|| + k) is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.z.|| is V11() real ext-real Element of REAL
t is Element of the carrier of X
z * t is Element of the carrier of X
k is Element of the carrier of X
p is V11() real ext-real Element of REAL
||.z.|| + 1 is V11() real ext-real Element of REAL
0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p / (||.z.|| + 1) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(z * s) . n is Element of the carrier of X
((z * s) . n) - k is Element of the carrier of X
||.(((z * s) . n) - k).|| is V11() real ext-real Element of REAL
s . n is Element of the carrier of X
(s . n) - t is Element of the carrier of X
||.((s . n) - t).|| is V11() real ext-real Element of REAL
z * ((s . n) - t) is Element of the carrier of X
||.(z * ((s . n) - t)).|| is V11() real ext-real Element of REAL
||.z.|| * ||.((s . n) - t).|| is V11() real ext-real Element of REAL
0 + ||.z.|| is V11() real ext-real Element of REAL
(||.z.|| + 1) * (p / (||.z.|| + 1)) is V11() real ext-real Element of REAL
||.z.|| * (p / (||.z.|| + 1)) is V11() real ext-real Element of REAL
(z * s) . n is Element of the carrier of X
((z * s) . n) - k is Element of the carrier of X
||.(((z * s) . n) - k).|| is V11() real ext-real Element of REAL
z * (s . n) is Element of the carrier of X
(z * (s . n)) - (z * t) is Element of the carrier of X
||.((z * (s . n)) - (z * t)).|| is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
s * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.z.|| is V11() real ext-real Element of REAL
t is Element of the carrier of X
t * z is Element of the carrier of X
k is Element of the carrier of X
p is V11() real ext-real Element of REAL
||.z.|| + 1 is V11() real ext-real Element of REAL
0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p / (||.z.|| + 1) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(s * z) . n is Element of the carrier of X
((s * z) . n) - k is Element of the carrier of X
||.(((s * z) . n) - k).|| is V11() real ext-real Element of REAL
s . n is Element of the carrier of X
(s . n) - t is Element of the carrier of X
||.((s . n) - t).|| is V11() real ext-real Element of REAL
((s . n) - t) * z is Element of the carrier of X
||.(((s . n) - t) * z).|| is V11() real ext-real Element of REAL
||.((s . n) - t).|| * ||.z.|| is V11() real ext-real Element of REAL
0 + ||.z.|| is V11() real ext-real Element of REAL
(p / (||.z.|| + 1)) * (||.z.|| + 1) is V11() real ext-real Element of REAL
(p / (||.z.|| + 1)) * ||.z.|| is V11() real ext-real Element of REAL
(s * z) . n is Element of the carrier of X
((s * z) . n) - k is Element of the carrier of X
||.(((s * z) . n) - k).|| is V11() real ext-real Element of REAL
(s . n) * z is Element of the carrier of X
((s . n) * z) - (t * z) is Element of the carrier of X
||.(((s . n) * z) - (t * z)).|| is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (z * s) is Element of the carrier of X
lim s is Element of the carrier of X
z * (lim s) is Element of the carrier of X
||.z.|| is V11() real ext-real Element of REAL
||.z.|| + 1 is V11() real ext-real Element of REAL
0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p is V11() real ext-real Element of REAL
p / (||.z.|| + 1) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . k is Element of the carrier of X
(s . k) - (lim s) is Element of the carrier of X
||.((s . k) - (lim s)).|| is V11() real ext-real Element of REAL
||.z.|| * ||.((s . k) - (lim s)).|| is V11() real ext-real Element of REAL
||.z.|| * (p / (||.z.|| + 1)) is V11() real ext-real Element of REAL
z * ((s . k) - (lim s)) is Element of the carrier of X
||.(z * ((s . k) - (lim s))).|| is V11() real ext-real Element of REAL
(z * s) . k is Element of the carrier of X
((z * s) . k) - (z * (lim s)) is Element of the carrier of X
||.(((z * s) . k) - (z * (lim s))).|| is V11() real ext-real Element of REAL
z * (s . k) is Element of the carrier of X
(z * (s . k)) - (z * (lim s)) is Element of the carrier of X
||.((z * (s . k)) - (z * (lim s))).|| is V11() real ext-real Element of REAL
0 + ||.z.|| is V11() real ext-real Element of REAL
(||.z.|| + 1) * (p / (||.z.|| + 1)) is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
s * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (s * z) is Element of the carrier of X
lim s is Element of the carrier of X
(lim s) * z is Element of the carrier of X
||.z.|| is V11() real ext-real Element of REAL
||.z.|| + 1 is V11() real ext-real Element of REAL
0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p is V11() real ext-real Element of REAL
p / (||.z.|| + 1) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . k is Element of the carrier of X
(s . k) - (lim s) is Element of the carrier of X
||.((s . k) - (lim s)).|| is V11() real ext-real Element of REAL
||.((s . k) - (lim s)).|| * ||.z.|| is V11() real ext-real Element of REAL
(p / (||.z.|| + 1)) * ||.z.|| is V11() real ext-real Element of REAL
((s . k) - (lim s)) * z is Element of the carrier of X
||.(((s . k) - (lim s)) * z).|| is V11() real ext-real Element of REAL
(s * z) . k is Element of the carrier of X
((s * z) . k) - ((lim s) * z) is Element of the carrier of X
||.(((s * z) . k) - ((lim s) * z)).|| is V11() real ext-real Element of REAL
(s . k) * z is Element of the carrier of X
((s . k) * z) - ((lim s) * z) is Element of the carrier of X
||.(((s . k) * z) - ((lim s) * z)).|| is V11() real ext-real Element of REAL
0 + ||.z.|| is V11() real ext-real Element of REAL
(p / (||.z.|| + 1)) * (||.z.|| + 1) is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim z is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (z * s) is Element of the carrier of X
lim s is Element of the carrier of X
(lim z) * (lim s) is Element of the carrier of X
||.z.|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
t is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z . n is Element of the carrier of X
||.(z . n).|| is V11() real ext-real Element of REAL
||.z.|| . n is V11() real ext-real Element of REAL
z . 1 is Element of the carrier of X
||.(z . 1).|| is V11() real ext-real Element of REAL
||.z.|| . 1 is V11() real ext-real Element of REAL
||.(lim s).|| is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
||.(lim s).|| + n is V11() real ext-real Element of REAL
0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
k is V11() real ext-real Element of REAL
k / (||.(lim s).|| + n) is V11() real ext-real Element of REAL
n4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n4 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z . l is Element of the carrier of X
(z . l) - (lim z) is Element of the carrier of X
||.((z . l) - (lim z)).|| is V11() real ext-real Element of REAL
||.(lim s).|| * ||.((z . l) - (lim z)).|| is V11() real ext-real Element of REAL
||.(lim s).|| * (k / (||.(lim s).|| + n)) is V11() real ext-real Element of REAL
((z . l) - (lim z)) * (lim s) is Element of the carrier of X
||.(((z . l) - (lim z)) * (lim s)).|| is V11() real ext-real Element of REAL
||.(z . l).|| is V11() real ext-real Element of REAL
(z * s) . l is Element of the carrier of X
((z * s) . l) - ((lim z) * (lim s)) is Element of the carrier of X
||.(((z * s) . l) - ((lim z) * (lim s))).|| is V11() real ext-real Element of REAL
s . l is Element of the carrier of X
(z . l) * (s . l) is Element of the carrier of X
((z . l) * (s . l)) - ((lim z) * (lim s)) is Element of the carrier of X
||.(((z . l) * (s . l)) - ((lim z) * (lim s))).|| is V11() real ext-real Element of REAL
(z . l) * (lim s) is Element of the carrier of X
((z . l) * (s . l)) - ((z . l) * (lim s)) is Element of the carrier of X
((z . l) * (lim s)) - ((lim z) * (lim s)) is Element of the carrier of X
(((z . l) * (s . l)) - ((z . l) * (lim s))) + (((z . l) * (lim s)) - ((lim z) * (lim s))) is Element of the carrier of X
||.((((z . l) * (s . l)) - ((z . l) * (lim s))) + (((z . l) * (lim s)) - ((lim z) * (lim s)))).|| is V11() real ext-real Element of REAL
(s . l) - (lim s) is Element of the carrier of X
(z . l) * ((s . l) - (lim s)) is Element of the carrier of X
((z . l) * ((s . l) - (lim s))) + (((z . l) * (lim s)) - ((lim z) * (lim s))) is Element of the carrier of X
||.(((z . l) * ((s . l) - (lim s))) + (((z . l) * (lim s)) - ((lim z) * (lim s)))).|| is V11() real ext-real Element of REAL
((z . l) * ((s . l) - (lim s))) + (((z . l) - (lim z)) * (lim s)) is Element of the carrier of X
||.(((z . l) * ((s . l) - (lim s))) + (((z . l) - (lim z)) * (lim s))).|| is V11() real ext-real Element of REAL
||.((z . l) * ((s . l) - (lim s))).|| is V11() real ext-real Element of REAL
||.((z . l) * ((s . l) - (lim s))).|| + ||.(((z . l) - (lim z)) * (lim s)).|| is V11() real ext-real Element of REAL
||.((s . l) - (lim s)).|| is V11() real ext-real Element of REAL
||.(z . l).|| * ||.((s . l) - (lim s)).|| is V11() real ext-real Element of REAL
n * (k / (||.(lim s).|| + n)) is V11() real ext-real Element of REAL
(n * (k / (||.(lim s).|| + n))) + (||.(lim s).|| * (k / (||.(lim s).|| + n))) is V11() real ext-real Element of REAL
(k / (||.(lim s).|| + n)) * (||.(lim s).|| + n) is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (z * s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
z * (Partial_Sums s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
s * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (s * z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums s) * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (s * z)) . t is Element of the carrier of X
((Partial_Sums s) * z) . t is Element of the carrier of X
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (s * z)) . (t + 1) is Element of the carrier of X
(s * z) . (t + 1) is Element of the carrier of X
((Partial_Sums (s * z)) . t) + ((s * z) . (t + 1)) is Element of the carrier of X
(Partial_Sums s) . t is Element of the carrier of X
((Partial_Sums s) . t) * z is Element of the carrier of X
(((Partial_Sums s) . t) * z) + ((s * z) . (t + 1)) is Element of the carrier of X
s . (t + 1) is Element of the carrier of X
(s . (t + 1)) * z is Element of the carrier of X
(((Partial_Sums s) . t) * z) + ((s . (t + 1)) * z) is Element of the carrier of X
((Partial_Sums s) . t) + (s . (t + 1)) is Element of the carrier of X
(((Partial_Sums s) . t) + (s . (t + 1))) * z is Element of the carrier of X
(Partial_Sums s) . (t + 1) is Element of the carrier of X
((Partial_Sums s) . (t + 1)) * z is Element of the carrier of X
((Partial_Sums s) * z) . (t + 1) is Element of the carrier of X
(Partial_Sums (s * z)) . 0 is Element of the carrier of X
(s * z) . 0 is Element of the carrier of X
s . 0 is Element of the carrier of X
(s . 0) * z is Element of the carrier of X
(Partial_Sums s) . 0 is Element of the carrier of X
((Partial_Sums s) . 0) * z is Element of the carrier of X
((Partial_Sums s) * z) . 0 is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (z * s)) . t is Element of the carrier of X
(z * (Partial_Sums s)) . t is Element of the carrier of X
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (z * s)) . (t + 1) is Element of the carrier of X
(z * s) . (t + 1) is Element of the carrier of X
((Partial_Sums (z * s)) . t) + ((z * s) . (t + 1)) is Element of the carrier of X
(Partial_Sums s) . t is Element of the carrier of X
z * ((Partial_Sums s) . t) is Element of the carrier of X
(z * ((Partial_Sums s) . t)) + ((z * s) . (t + 1)) is Element of the carrier of X
s . (t + 1) is Element of the carrier of X
z * (s . (t + 1)) is Element of the carrier of X
(z * ((Partial_Sums s) . t)) + (z * (s . (t + 1))) is Element of the carrier of X
((Partial_Sums s) . t) + (s . (t + 1)) is Element of the carrier of X
z * (((Partial_Sums s) . t) + (s . (t + 1))) is Element of the carrier of X
(Partial_Sums s) . (t + 1) is Element of the carrier of X
z * ((Partial_Sums s) . (t + 1)) is Element of the carrier of X
(z * (Partial_Sums s)) . (t + 1) is Element of the carrier of X
(Partial_Sums (z * s)) . 0 is Element of the carrier of X
(z * s) . 0 is Element of the carrier of X
s . 0 is Element of the carrier of X
z * (s . 0) is Element of the carrier of X
(Partial_Sums s) . 0 is Element of the carrier of X
z * ((Partial_Sums s) . 0) is Element of the carrier of X
(z * (Partial_Sums s)) . 0 is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums s) . z is Element of the carrier of X
||.((Partial_Sums s) . z).|| is V11() real ext-real Element of REAL
||.s.|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.s.|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.s.||) . z is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums s) . t is Element of the carrier of X
||.((Partial_Sums s) . t).|| is V11() real ext-real Element of REAL
(Partial_Sums ||.s.||) . t is V11() real ext-real Element of REAL
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . (t + 1) is Element of the carrier of X
||.(s . (t + 1)).|| is V11() real ext-real Element of REAL
||.((Partial_Sums s) . t).|| + ||.(s . (t + 1)).|| is V11() real ext-real Element of REAL
((Partial_Sums ||.s.||) . t) + ||.(s . (t + 1)).|| is V11() real ext-real Element of REAL
((Partial_Sums s) . t) + (s . (t + 1)) is Element of the carrier of X
||.(((Partial_Sums s) . t) + (s . (t + 1))).|| is V11() real ext-real Element of REAL
(Partial_Sums s) . (t + 1) is Element of the carrier of X
||.((Partial_Sums s) . (t + 1)).|| is V11() real ext-real Element of REAL
||.s.|| . (t + 1) is V11() real ext-real Element of REAL
((Partial_Sums ||.s.||) . t) + (||.s.|| . (t + 1)) is V11() real ext-real Element of REAL
(Partial_Sums ||.s.||) . (t + 1) is V11() real ext-real Element of REAL
(Partial_Sums ||.s.||) . 0 is V11() real ext-real Element of REAL
||.s.|| . 0 is V11() real ext-real Element of REAL
s . 0 is Element of the carrier of X
||.(s . 0).|| is V11() real ext-real Element of REAL
(Partial_Sums s) . 0 is Element of the carrier of X
||.((Partial_Sums s) . 0).|| is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums s) . z is Element of the carrier of X
t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums t) . z is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums s) . k is Element of the carrier of X
(Partial_Sums t) . k is Element of the carrier of X
k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums s) . (k + 1) is Element of the carrier of X
(Partial_Sums t) . (k + 1) is Element of the carrier of X
s . (k + 1) is Element of the carrier of X
((Partial_Sums t) . k) + (s . (k + 1)) is Element of the carrier of X
t . (k + 1) is Element of the carrier of X
((Partial_Sums t) . k) + (t . (k + 1)) is Element of the carrier of X
(Partial_Sums s) . 0 is Element of the carrier of X
(Partial_Sums t) . 0 is Element of the carrier of X
s . 0 is Element of the carrier of X
t . 0 is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
0. X is V82(X) Element of the carrier of X
z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim z is Element of the carrier of X
s is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim s is V11() real ext-real Element of REAL
t is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . p is V11() real ext-real Element of REAL
(s . p) - 0 is V11() real ext-real Element of REAL
abs ((s . p) - 0) is V11() real ext-real Element of REAL
z . p is Element of the carrier of X
(z . p) - (0. X) is Element of the carrier of X
||.((z . p) - (0. X)).|| is V11() real ext-real Element of REAL
||.(z . p).|| is V11() real ext-real Element of REAL
abs (s . p) is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . k is Element of the carrier of X
t . k is Element of the carrier of X
z #N k is Element of the carrier of X
z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(z GeoSeq) . k is Element of the carrier of X
k ! is V11() real ext-real Element of REAL
1 / (k !) is V11() real ext-real Element of REAL
(1 / (k !)) * (z #N k) is Element of the carrier of X
F₁() is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of F₁() is V1() set
K7(NAT, the carrier of F₁()) is set
K6(K7(NAT, the carrier of F₁())) is set
0. F₁() is V82(F₁()) Element of the carrier of F₁()
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z is set
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
CHK (s,X) is V11() real ext-real Element of COMPLEX
F₂(X,s) is Element of the carrier of F₁()
t is V11() real ext-real Element of REAL
t * F₂(X,s) is Element of the carrier of F₁()
0 * F₂(X,s) is Element of the carrier of F₁()
k is set
1 * F₂(X,s) is Element of the carrier of F₁()
p is set
z is Relation-like Function-like set
dom z is set
s is set
z . s is set
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
F₂(X,t) is Element of the carrier of F₁()
s is V1() Relation-like NAT -defined the carrier of F₁() -valued Function-like V26( NAT ) V30( NAT , the carrier of F₁()) Element of K6(K7(NAT, the carrier of F₁()))
t is V1() Relation-like NAT -defined the carrier of F₁() -valued Function-like V26( NAT ) V30( NAT , the carrier of F₁()) Element of K6(K7(NAT, the carrier of F₁()))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t . k is Element of the carrier of F₁()
F₂(X,k) is Element of the carrier of F₁()
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
F₂(X,p) is Element of the carrier of F₁()
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X -' 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X - 1 is V11() real ext-real Element of REAL
(X - 1) + 1 is V11() real ext-real Element of REAL
X ! is V11() real ext-real Element of REAL
(X -' 1) ! is V11() real ext-real Element of REAL
((X -' 1) !) * X is V11() real ext-real Element of REAL
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X + 1) -' z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X + 1) - z is V11() real ext-real Element of REAL
X - z is V11() real ext-real Element of REAL
(X - z) + 1 is V11() real ext-real Element of REAL
X -' z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X -' z) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((X + 1) -' z) ! is V11() real ext-real Element of REAL
(X -' z) ! is V11() real ext-real Element of REAL
((X -' z) !) * ((X -' z) + 1) is V11() real ext-real Element of REAL
((X -' z) !) * ((X - z) + 1) is V11() real ext-real Element of REAL
((X -' z) !) * ((X + 1) - z) is V11() real ext-real Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X -' 1) ! is V11() real ext-real Element of REAL
((X -' 1) !) * X is V11() real ext-real Element of REAL
X ! is V11() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z -' s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(z -' s) ! is V11() real ext-real Element of REAL
z + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(z + 1) - s is V11() real ext-real Element of REAL
((z -' s) !) * ((z + 1) - s) is V11() real ext-real Element of REAL
(z + 1) -' s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((z + 1) -' s) ! is V11() real ext-real Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X ! is V11() real ext-real Element of REAL
z is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
s is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z . t is V11() real ext-real Element of REAL
t ! is V11() real ext-real Element of REAL
X -' t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X -' t) ! is V11() real ext-real Element of REAL
(t !) * ((X -' t) !) is V11() real ext-real Element of REAL
(X !) / ((t !) * ((X -' t) !)) is V11() real ext-real Element of REAL
s . t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z . t is V11() real ext-real Element of REAL
s . t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
s is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z . t is V11() real ext-real Element of REAL
t ! is V11() real ext-real Element of REAL
X -' t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X -' t) ! is V11() real ext-real Element of REAL
(t !) * ((X -' t) !) is V11() real ext-real Element of REAL
1 / ((t !) * ((X -' t) !)) is V11() real ext-real Element of REAL
s . t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z . t is V11() real ext-real Element of REAL
s . t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X is non empty ZeroStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
0. X is V82(X) Element of the carrier of X
z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
s . 0 is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . (t + 1) is Element of the carrier of X
z . t is Element of the carrier of X
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
s . 0 is Element of the carrier of X
t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
t . 0 is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . k is Element of the carrier of X
t . k is Element of the carrier of X
k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . (k + 1) is Element of the carrier of X
t . (k + 1) is Element of the carrier of X
z . k is Element of the carrier of X
z is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of z is V1() set
K7(NAT, the carrier of z) is set
K6(K7(NAT, the carrier of z)) is set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of z
(X) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
t is Element of the carrier of z
0. z is V82(z) Element of the carrier of z
k is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
p is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . n is Element of the carrier of z
s #N n is Element of the carrier of z
s GeoSeq is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
(s GeoSeq) . n is Element of the carrier of z
(X) . n is V11() real ext-real Element of REAL
((X) . n) * (s #N n) is Element of the carrier of z
X -' n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t #N (X -' n) is Element of the carrier of z
t GeoSeq is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
(t GeoSeq) . (X -' n) is Element of the carrier of z
(((X) . n) * (s #N n)) * (t #N (X -' n)) is Element of the carrier of z
p . n is Element of the carrier of z
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . n is Element of the carrier of z
p . n is Element of the carrier of z
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of z is V1() set
K7(NAT, the carrier of z) is set
K6(K7(NAT, the carrier of z)) is set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of z
(X) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
t is Element of the carrier of z
0. z is V82(z) Element of the carrier of z
k is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
p is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . n is Element of the carrier of z
s #N n is Element of the carrier of z
s GeoSeq is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
(s GeoSeq) . n is Element of the carrier of z
(X) . n is V11() real ext-real Element of REAL
((X) . n) * (s #N n) is Element of the carrier of z
X -' n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t #N (X -' n) is Element of the carrier of z
t GeoSeq is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
(t GeoSeq) . (X -' n) is Element of the carrier of z
(((X) . n) * (s #N n)) * (t #N (X -' n)) is Element of the carrier of z
p . n is Element of the carrier of z
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . n is Element of the carrier of z
p . n is Element of the carrier of z
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of z is V1() set
K7(NAT, the carrier of z) is set
K6(K7(NAT, the carrier of z)) is set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of z
(z,s) is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
t is Element of the carrier of z
(z,t) is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
Partial_Sums (z,t) is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
0. z is V82(z) Element of the carrier of z
k is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
p is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . n is Element of the carrier of z
(z,s) . n is Element of the carrier of z
X -' n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (z,t)) . (X -' n) is Element of the carrier of z
((z,s) . n) * ((Partial_Sums (z,t)) . (X -' n)) is Element of the carrier of z
p . n is Element of the carrier of z
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . n is Element of the carrier of z
p . n is Element of the carrier of z
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
s is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,s)) . t is Element of the carrier of X
0. X is V82(X) Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
p is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . n is Element of the carrier of X
(X,z) . n is Element of the carrier of X
t -' n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,s)) . (t -' n) is Element of the carrier of X
((Partial_Sums (X,s)) . t) - ((Partial_Sums (X,s)) . (t -' n)) is Element of the carrier of X
((X,z) . n) * (((Partial_Sums (X,s)) . t) - ((Partial_Sums (X,s)) . (t -' n))) is Element of the carrier of X
p . n is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . n is Element of the carrier of X
p . n is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
1. X is Element of the carrier of X
z is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
(X,z) . 0 is Element of the carrier of X
||.z.|| is V11() real ext-real Element of REAL
||.z.|| rExpSeq is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z) . (s + 1) is Element of the carrier of X
1 / (s + 1) is V11() real ext-real non negative Element of REAL
(1 / (s + 1)) * z is Element of the carrier of X
(X,z) . s is Element of the carrier of X
((1 / (s + 1)) * z) * ((X,z) . s) is Element of the carrier of X
||.((X,z) . s).|| is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . s is V11() real ext-real Element of REAL
z #N 0 is Element of the carrier of X
z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(z GeoSeq) . 0 is Element of the carrier of X
1 / (0 !) is V11() real ext-real Element of REAL
(1 / (0 !)) * (z #N 0) is Element of the carrier of X
1 / 1 is V11() real ext-real non negative Element of REAL
(1 / 1) * (1. X) is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z) . (t + 1) is Element of the carrier of X
z #N (t + 1) is Element of the carrier of X
(z GeoSeq) . (t + 1) is Element of the carrier of X
(t + 1) ! is V11() real ext-real Element of REAL
1 / ((t + 1) !) is V11() real ext-real Element of REAL
(1 / ((t + 1) !)) * (z #N (t + 1)) is Element of the carrier of X
(z GeoSeq) . t is Element of the carrier of X
((z GeoSeq) . t) * z is Element of the carrier of X
(1 / ((t + 1) !)) * (((z GeoSeq) . t) * z) is Element of the carrier of X
z #N t is Element of the carrier of X
(z GeoSeq) . t is Element of the carrier of X
(z #N t) * z is Element of the carrier of X
t ! is V11() real ext-real Element of REAL
(t !) * (t + 1) is V11() real ext-real Element of REAL
1 / ((t !) * (t + 1)) is V11() real ext-real Element of REAL
(1 / ((t !) * (t + 1))) * ((z #N t) * z) is Element of the carrier of X
z * (z #N t) is Element of the carrier of X
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(1 * 1) / ((t !) * (t + 1)) is V11() real ext-real Element of REAL
((1 * 1) / ((t !) * (t + 1))) * (z * (z #N t)) is Element of the carrier of X
1 / (t !) is V11() real ext-real Element of REAL
1 / (t + 1) is V11() real ext-real non negative Element of REAL
(1 / (t !)) * (1 / (t + 1)) is V11() real ext-real Element of REAL
((1 / (t !)) * (1 / (t + 1))) * (z * (z #N t)) is Element of the carrier of X
(1 / (t + 1)) * z is Element of the carrier of X
(1 / (t !)) * (z #N t) is Element of the carrier of X
((1 / (t + 1)) * z) * ((1 / (t !)) * (z #N t)) is Element of the carrier of X
(X,z) . t is Element of the carrier of X
((1 / (t + 1)) * z) * ((X,z) . t) is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z) . t is Element of the carrier of X
||.((X,z) . t).|| is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . t is V11() real ext-real Element of REAL
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z) . (t + 1) is Element of the carrier of X
||.((X,z) . (t + 1)).|| is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . (t + 1) is V11() real ext-real Element of REAL
1 / (t + 1) is V11() real ext-real non negative Element of REAL
(1 / (t + 1)) * z is Element of the carrier of X
||.((1 / (t + 1)) * z).|| is V11() real ext-real Element of REAL
||.((1 / (t + 1)) * z).|| * ||.((X,z) . t).|| is V11() real ext-real Element of REAL
||.((1 / (t + 1)) * z).|| * ((||.z.|| rExpSeq) . t) is V11() real ext-real Element of REAL
((1 / (t + 1)) * z) * ((X,z) . t) is Element of the carrier of X
||.(((1 / (t + 1)) * z) * ((X,z) . t)).|| is V11() real ext-real Element of REAL
(1 / (t + 1)) * ||.z.|| is V11() real ext-real Element of REAL
((1 / (t + 1)) * ||.z.||) * ((||.z.|| rExpSeq) . t) is V11() real ext-real Element of REAL
((||.z.|| rExpSeq) . t) * ||.z.|| is V11() real ext-real Element of REAL
(1 / (t + 1)) * (((||.z.|| rExpSeq) . t) * ||.z.||) is V11() real ext-real Element of REAL
||.z.|| |^ t is V11() real ext-real Element of REAL
t ! is V11() real ext-real Element of REAL
(||.z.|| |^ t) / (t !) is V11() real ext-real Element of REAL
((||.z.|| |^ t) / (t !)) * ||.z.|| is V11() real ext-real Element of REAL
(1 / (t + 1)) * (((||.z.|| |^ t) / (t !)) * ||.z.||) is V11() real ext-real Element of REAL
(||.z.|| |^ t) * ||.z.|| is V11() real ext-real Element of REAL
((||.z.|| |^ t) * ||.z.||) / (t !) is V11() real ext-real Element of REAL
(1 / (t + 1)) * (((||.z.|| |^ t) * ||.z.||) / (t !)) is V11() real ext-real Element of REAL
||.z.|| |^ (t + 1) is V11() real ext-real Element of REAL
(||.z.|| |^ (t + 1)) / (t !) is V11() real ext-real Element of REAL
(1 / (t + 1)) * ((||.z.|| |^ (t + 1)) / (t !)) is V11() real ext-real Element of REAL
(t !) * (t + 1) is V11() real ext-real Element of REAL
(||.z.|| |^ (t + 1)) / ((t !) * (t + 1)) is V11() real ext-real Element of REAL
(t + 1) ! is V11() real ext-real Element of REAL
(||.z.|| |^ (t + 1)) / ((t + 1) !) is V11() real ext-real Element of REAL
abs (1 / (t + 1)) is V11() real ext-real Element of REAL
(abs (1 / (t + 1))) * ||.z.|| is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . 0 is V11() real ext-real Element of REAL
||.z.|| |^ 0 is V11() real ext-real Element of REAL
(||.z.|| |^ 0) / (0 !) is V11() real ext-real Element of REAL
Prod_real_n . 0 is V11() real ext-real Element of REAL
1 / (Prod_real_n . 0) is V11() real ext-real Element of REAL
||.((X,z) . 0).|| is V11() real ext-real Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z is non empty ZeroStr
the carrier of z is V1() set
K7(NAT, the carrier of z) is set
K6(K7(NAT, the carrier of z)) is set
s is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
(z,s) is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))
(z,s) . X is Element of the carrier of z
s . (X -' 1) is Element of the carrier of z
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X - 1 is V11() real ext-real Element of REAL
s . t is Element of the carrier of z
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums s) . z is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,s)) . z is Element of the carrier of X
s . z is Element of the carrier of X
((Partial_Sums (X,s)) . z) + (s . z) is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums s) . t is Element of the carrier of X
(Partial_Sums (X,s)) . t is Element of the carrier of X
s . t is Element of the carrier of X
((Partial_Sums (X,s)) . t) + (s . t) is Element of the carrier of X
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums s) . (t + 1) is Element of the carrier of X
(Partial_Sums (X,s)) . (t + 1) is Element of the carrier of X
s . (t + 1) is Element of the carrier of X
((Partial_Sums (X,s)) . (t + 1)) + (s . (t + 1)) is Element of the carrier of X
(((Partial_Sums (X,s)) . t) + (s . t)) + (s . (t + 1)) is Element of the carrier of X
(X,s) . (t + 1) is Element of the carrier of X
((Partial_Sums (X,s)) . t) + ((X,s) . (t + 1)) is Element of the carrier of X
(((Partial_Sums (X,s)) . t) + ((X,s) . (t + 1))) + (s . (t + 1)) is Element of the carrier of X
(Partial_Sums s) . 0 is Element of the carrier of X
s . 0 is Element of the carrier of X
0. X is V82(X) Element of the carrier of X
(0. X) + (s . 0) is Element of the carrier of X
(X,s) . 0 is Element of the carrier of X
((X,s) . 0) + (s . 0) is Element of the carrier of X
(Partial_Sums (X,s)) . 0 is Element of the carrier of X
((Partial_Sums (X,s)) . 0) + (s . 0) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of X
t is Element of the carrier of X
s + t is Element of the carrier of X
(s + t) #N z is Element of the carrier of X
(s + t) GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
((s + t) GeoSeq) . z is Element of the carrier of X
(z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (z,X,s,t)) . z is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(s + t) #N k is Element of the carrier of X
((s + t) GeoSeq) . k is Element of the carrier of X
(k,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (k,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (k,X,s,t)) . k is Element of the carrier of X
k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(s + t) #N (k + 1) is Element of the carrier of X
((s + t) GeoSeq) . (k + 1) is Element of the carrier of X
((k + 1),X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums ((k + 1),X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((k + 1),X,s,t)) . (k + 1) is Element of the carrier of X
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p ! is V11() real ext-real Element of REAL
k -' p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k -' p) ! is V11() real ext-real Element of REAL
(p !) * ((k -' p) !) is V11() real ext-real Element of REAL
(k + 1) - p is V11() real ext-real Element of REAL
((p !) * ((k -' p) !)) * ((k + 1) - p) is V11() real ext-real Element of REAL
((k -' p) !) * ((k + 1) - p) is V11() real ext-real Element of REAL
(p !) * (((k -' p) !) * ((k + 1) - p)) is V11() real ext-real Element of REAL
p + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(p + 1) - 1 is V11() real ext-real Element of REAL
(k + 1) - 1 is V11() real ext-real Element of REAL
(k -' p) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - p is V11() real ext-real Element of REAL
(k - p) + 1 is V11() real ext-real Element of REAL
(k + 1) -' p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k ! is V11() real ext-real Element of REAL
(k !) / ((p !) * ((k -' p) !)) is V11() real ext-real Element of REAL
(k !) * ((k + 1) - p) is V11() real ext-real Element of REAL
((k !) * ((k + 1) - p)) / (((p !) * ((k -' p) !)) * ((k + 1) - p)) is V11() real ext-real Element of REAL
((k + 1) -' p) ! is V11() real ext-real Element of REAL
(p !) * (((k + 1) -' p) !) is V11() real ext-real Element of REAL
((k !) * ((k + 1) - p)) / ((p !) * (((k + 1) -' p) !)) is V11() real ext-real Element of REAL
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(p -' 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p - 1 is V11() real ext-real Element of REAL
(p - 1) + 1 is V11() real ext-real Element of REAL
k -' (p -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - (p -' 1) is V11() real ext-real Element of REAL
k - (p - 1) is V11() real ext-real Element of REAL
(p -' 1) ! is V11() real ext-real Element of REAL
(k -' (p -' 1)) ! is V11() real ext-real Element of REAL
((p -' 1) !) * ((k -' (p -' 1)) !) is V11() real ext-real Element of REAL
(((p -' 1) !) * ((k -' (p -' 1)) !)) * p is V11() real ext-real Element of REAL
p * ((p -' 1) !) is V11() real ext-real Element of REAL
(p * ((p -' 1) !)) * ((k -' (p -' 1)) !) is V11() real ext-real Element of REAL
(k !) / (((p -' 1) !) * ((k -' (p -' 1)) !)) is V11() real ext-real Element of REAL
(k !) * p is V11() real ext-real Element of REAL
((k !) * p) / ((p !) * (((k + 1) -' p) !)) is V11() real ext-real Element of REAL
(k,X,s,t) * t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(k,X,s,t) * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((k,X,s,t) * s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((k,X,s,t) * t) + (X,((k,X,s,t) * s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(((k,X,s,t) * t) + (X,((k,X,s,t) * s))) . p is Element of the carrier of X
((k,X,s,t) * t) . p is Element of the carrier of X
(X,((k,X,s,t) * s)) . p is Element of the carrier of X
(((k,X,s,t) * t) . p) + ((X,((k,X,s,t) * s)) . p) is Element of the carrier of X
(k,X,s,t) . p is Element of the carrier of X
((k,X,s,t) . p) * t is Element of the carrier of X
(((k,X,s,t) . p) * t) + ((X,((k,X,s,t) * s)) . p) is Element of the carrier of X
((k,X,s,t) * s) . (p -' 1) is Element of the carrier of X
(((k,X,s,t) . p) * t) + (((k,X,s,t) * s) . (p -' 1)) is Element of the carrier of X
(k,X,s,t) . (p -' 1) is Element of the carrier of X
((k,X,s,t) . (p -' 1)) * s is Element of the carrier of X
(((k,X,s,t) . p) * t) + (((k,X,s,t) . (p -' 1)) * s) is Element of the carrier of X
s #N p is Element of the carrier of X
s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(s GeoSeq) . p is Element of the carrier of X
(k) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(k) . p is V11() real ext-real Element of REAL
((k) . p) * (s #N p) is Element of the carrier of X
t #N (k -' p) is Element of the carrier of X
t GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(t GeoSeq) . (k -' p) is Element of the carrier of X
(((k) . p) * (s #N p)) * (t #N (k -' p)) is Element of the carrier of X
((((k) . p) * (s #N p)) * (t #N (k -' p))) * t is Element of the carrier of X
(((((k) . p) * (s #N p)) * (t #N (k -' p))) * t) + (((k,X,s,t) . (p -' 1)) * s) is Element of the carrier of X
s #N (p -' 1) is Element of the carrier of X
(s GeoSeq) . (p -' 1) is Element of the carrier of X
(k) . (p -' 1) is V11() real ext-real Element of REAL
((k) . (p -' 1)) * (s #N (p -' 1)) is Element of the carrier of X
t #N (k -' (p -' 1)) is Element of the carrier of X
(t GeoSeq) . (k -' (p -' 1)) is Element of the carrier of X
(((k) . (p -' 1)) * (s #N (p -' 1))) * (t #N (k -' (p -' 1))) is Element of the carrier of X
((((k) . (p -' 1)) * (s #N (p -' 1))) * (t #N (k -' (p -' 1)))) * s is Element of the carrier of X
(((((k) . p) * (s #N p)) * (t #N (k -' p))) * t) + (((((k) . (p -' 1)) * (s #N (p -' 1))) * (t #N (k -' (p -' 1)))) * s) is Element of the carrier of X
(t #N (k -' p)) * t is Element of the carrier of X
(((k) . p) * (s #N p)) * ((t #N (k -' p)) * t) is Element of the carrier of X
((((k) . p) * (s #N p)) * ((t #N (k -' p)) * t)) + (((((k) . (p -' 1)) * (s #N (p -' 1))) * (t #N (k -' (p -' 1)))) * s) is Element of the carrier of X
t #N ((k -' p) + 1) is Element of the carrier of X
(t GeoSeq) . ((k -' p) + 1) is Element of the carrier of X
(((k) . p) * (s #N p)) * (t #N ((k -' p) + 1)) is Element of the carrier of X
((((k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + (((((k) . (p -' 1)) * (s #N (p -' 1))) * (t #N (k -' (p -' 1)))) * s) is Element of the carrier of X
(t #N (k -' (p -' 1))) * s is Element of the carrier of X
(((k) . (p -' 1)) * (s #N (p -' 1))) * ((t #N (k -' (p -' 1))) * s) is Element of the carrier of X
((((k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + ((((k) . (p -' 1)) * (s #N (p -' 1))) * ((t #N (k -' (p -' 1))) * s)) is Element of the carrier of X
s * (t #N (k -' (p -' 1))) is Element of the carrier of X
(((k) . (p -' 1)) * (s #N (p -' 1))) * (s * (t #N (k -' (p -' 1)))) is Element of the carrier of X
((((k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + ((((k) . (p -' 1)) * (s #N (p -' 1))) * (s * (t #N (k -' (p -' 1))))) is Element of the carrier of X
(((k) . (p -' 1)) * (s #N (p -' 1))) * s is Element of the carrier of X
((((k) . (p -' 1)) * (s #N (p -' 1))) * s) * (t #N (k -' (p -' 1))) is Element of the carrier of X
((((k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + (((((k) . (p -' 1)) * (s #N (p -' 1))) * s) * (t #N (k -' (p -' 1)))) is Element of the carrier of X
(s #N (p -' 1)) * s is Element of the carrier of X
((k) . (p -' 1)) * ((s #N (p -' 1)) * s) is Element of the carrier of X
(((k) . (p -' 1)) * ((s #N (p -' 1)) * s)) * (t #N (k -' (p -' 1))) is Element of the carrier of X
((((k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + ((((k) . (p -' 1)) * ((s #N (p -' 1)) * s)) * (t #N (k -' (p -' 1)))) is Element of the carrier of X
s #N ((p -' 1) + 1) is Element of the carrier of X
(s GeoSeq) . ((p -' 1) + 1) is Element of the carrier of X
((k) . (p -' 1)) * (s #N ((p -' 1) + 1)) is Element of the carrier of X
(((k) . (p -' 1)) * (s #N ((p -' 1) + 1))) * (t #N (k -' (p -' 1))) is Element of the carrier of X
((((k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + ((((k) . (p -' 1)) * (s #N ((p -' 1) + 1))) * (t #N (k -' (p -' 1)))) is Element of the carrier of X
t #N ((k + 1) -' p) is Element of the carrier of X
(t GeoSeq) . ((k + 1) -' p) is Element of the carrier of X
(s #N p) * (t #N ((k + 1) -' p)) is Element of the carrier of X
((k) . p) * ((s #N p) * (t #N ((k + 1) -' p))) is Element of the carrier of X
((k) . (p -' 1)) * (s #N p) is Element of the carrier of X
(((k) . (p -' 1)) * (s #N p)) * (t #N ((k + 1) -' p)) is Element of the carrier of X
(((k) . p) * ((s #N p) * (t #N ((k + 1) -' p)))) + ((((k) . (p -' 1)) * (s #N p)) * (t #N ((k + 1) -' p))) is Element of the carrier of X
((k) . (p -' 1)) * ((s #N p) * (t #N ((k + 1) -' p))) is Element of the carrier of X
(((k) . p) * ((s #N p) * (t #N ((k + 1) -' p)))) + (((k) . (p -' 1)) * ((s #N p) * (t #N ((k + 1) -' p)))) is Element of the carrier of X
((k) . p) + ((k) . (p -' 1)) is V11() real ext-real Element of REAL
(((k) . p) + ((k) . (p -' 1))) * ((s #N p) * (t #N ((k + 1) -' p))) is Element of the carrier of X
((k !) / ((p !) * ((k -' p) !))) + ((k) . (p -' 1)) is V11() real ext-real Element of REAL
((k !) / ((p !) * ((k -' p) !))) + ((k !) / (((p -' 1) !) * ((k -' (p -' 1)) !))) is V11() real ext-real Element of REAL
((k !) * ((k + 1) - p)) + ((k !) * p) is V11() real ext-real Element of REAL
(((k !) * ((k + 1) - p)) + ((k !) * p)) / ((p !) * (((k + 1) -' p) !)) is V11() real ext-real Element of REAL
((k + 1) - p) + p is V11() real ext-real Element of REAL
(k !) * (((k + 1) - p) + p) is V11() real ext-real Element of REAL
((k !) * (((k + 1) - p) + p)) / ((p !) * (((k + 1) -' p) !)) is V11() real ext-real Element of REAL
(k + 1) ! is V11() real ext-real Element of REAL
((k + 1) !) / ((p !) * (((k + 1) -' p) !)) is V11() real ext-real Element of REAL
((k + 1)) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((k + 1)) . p is V11() real ext-real Element of REAL
(((k + 1)) . p) * (s #N p) is Element of the carrier of X
((((k + 1)) . p) * (s #N p)) * (t #N ((k + 1) -' p)) is Element of the carrier of X
((k + 1),X,s,t) . p is Element of the carrier of X
(k + 1) -' 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k + 1) - 0 is V1() V11() real ext-real positive non negative Element of REAL
((k + 1)) . 0 is V11() real ext-real Element of REAL
(0 !) * ((k + 1) !) is V11() real ext-real Element of REAL
((k + 1) !) / ((0 !) * ((k + 1) !)) is V11() real ext-real Element of REAL
k -' 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - 0 is V11() real ext-real non negative Element of REAL
(k) . 0 is V11() real ext-real Element of REAL
(0 !) * (k !) is V11() real ext-real Element of REAL
(k !) / ((0 !) * (k !)) is V11() real ext-real Element of REAL
((k,X,s,t) * t) . 0 is Element of the carrier of X
(X,((k,X,s,t) * s)) . 0 is Element of the carrier of X
(((k,X,s,t) * t) . 0) + ((X,((k,X,s,t) * s)) . 0) is Element of the carrier of X
(k,X,s,t) . 0 is Element of the carrier of X
((k,X,s,t) . 0) * t is Element of the carrier of X
(((k,X,s,t) . 0) * t) + ((X,((k,X,s,t) * s)) . 0) is Element of the carrier of X
0. X is V82(X) Element of the carrier of X
(((k,X,s,t) . 0) * t) + (0. X) is Element of the carrier of X
s #N 0 is Element of the carrier of X
(s GeoSeq) . 0 is Element of the carrier of X
((k) . 0) * (s #N 0) is Element of the carrier of X
t #N (k -' 0) is Element of the carrier of X
(t GeoSeq) . (k -' 0) is Element of the carrier of X
(((k) . 0) * (s #N 0)) * (t #N (k -' 0)) is Element of the carrier of X
((((k) . 0) * (s #N 0)) * (t #N (k -' 0))) * t is Element of the carrier of X
(t #N (k -' 0)) * t is Element of the carrier of X
(((k) . 0) * (s #N 0)) * ((t #N (k -' 0)) * t) is Element of the carrier of X
(((k + 1)) . 0) * (s #N 0) is Element of the carrier of X
t #N ((k + 1) -' 0) is Element of the carrier of X
(t GeoSeq) . ((k + 1) -' 0) is Element of the carrier of X
((((k + 1)) . 0) * (s #N 0)) * (t #N ((k + 1) -' 0)) is Element of the carrier of X
(k + 1) -' (k + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k + 1) - (k + 1) is V11() real ext-real Element of REAL
((k + 1)) . (k + 1) is V11() real ext-real Element of REAL
((k + 1) !) * (0 !) is V11() real ext-real Element of REAL
((k + 1) !) / (((k + 1) !) * (0 !)) is V11() real ext-real Element of REAL
k -' k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - k is V11() real ext-real Element of REAL
(k) . k is V11() real ext-real Element of REAL
(k !) * (0 !) is V11() real ext-real Element of REAL
(k !) / ((k !) * (0 !)) is V11() real ext-real Element of REAL
((k,X,s,t) * t) . (k + 1) is Element of the carrier of X
(X,((k,X,s,t) * s)) . (k + 1) is Element of the carrier of X
(((k,X,s,t) * t) . (k + 1)) + ((X,((k,X,s,t) * s)) . (k + 1)) is Element of the carrier of X
(k,X,s,t) . (k + 1) is Element of the carrier of X
((k,X,s,t) . (k + 1)) * t is Element of the carrier of X
(((k,X,s,t) . (k + 1)) * t) + ((X,((k,X,s,t) * s)) . (k + 1)) is Element of the carrier of X
(0. X) * t is Element of the carrier of X
((0. X) * t) + ((X,((k,X,s,t) * s)) . (k + 1)) is Element of the carrier of X
(0. X) + ((X,((k,X,s,t) * s)) . (k + 1)) is Element of the carrier of X
((k,X,s,t) * s) . k is Element of the carrier of X
(k,X,s,t) . k is Element of the carrier of X
((k,X,s,t) . k) * s is Element of the carrier of X
s #N k is Element of the carrier of X
(s GeoSeq) . k is Element of the carrier of X
((k) . k) * (s #N k) is Element of the carrier of X
t #N (k -' k) is Element of the carrier of X
(t GeoSeq) . (k -' k) is Element of the carrier of X
(((k) . k) * (s #N k)) * (t #N (k -' k)) is Element of the carrier of X
((((k) . k) * (s #N k)) * (t #N (k -' k))) * s is Element of the carrier of X
(t #N (k -' k)) * s is Element of the carrier of X
(((k) . k) * (s #N k)) * ((t #N (k -' k)) * s) is Element of the carrier of X
s * (t #N (k -' k)) is Element of the carrier of X
(((k) . k) * (s #N k)) * (s * (t #N (k -' k))) is Element of the carrier of X
(((k) . k) * (s #N k)) * s is Element of the carrier of X
((((k) . k) * (s #N k)) * s) * (t #N (k -' k)) is Element of the carrier of X
(s #N k) * s is Element of the carrier of X
((k) . k) * ((s #N k) * s) is Element of the carrier of X
(((k) . k) * ((s #N k) * s)) * (t #N (k -' k)) is Element of the carrier of X
s #N (k + 1) is Element of the carrier of X
(s GeoSeq) . (k + 1) is Element of the carrier of X
(((k + 1)) . (k + 1)) * (s #N (k + 1)) is Element of the carrier of X
((((k + 1)) . (k + 1)) * (s #N (k + 1))) * (t #N (k -' k)) is Element of the carrier of X
k + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((0. X) * t) + (((k,X,s,t) . (p -' 1)) * s) is Element of the carrier of X
(0. X) + (((k,X,s,t) . (p -' 1)) * s) is Element of the carrier of X
(0. X) * s is Element of the carrier of X
(0. X) + ((0. X) * s) is Element of the carrier of X
(0. X) + (0. X) is Element of the carrier of X
Partial_Sums ((k,X,s,t) * t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((k,X,s,t) * t)) . (k + 1) is Element of the carrier of X
(Partial_Sums ((k,X,s,t) * t)) . k is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * t)) . k) + (((k,X,s,t) * t) . (k + 1)) is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * t)) . k) + (((k,X,s,t) . (k + 1)) * t) is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * t)) . k) + ((0. X) * t) is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * t)) . k) + (0. X) is Element of the carrier of X
Partial_Sums ((k,X,s,t) * s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((k,X,s,t) * s)) . (k + 1) is Element of the carrier of X
(Partial_Sums ((k,X,s,t) * s)) . k is Element of the carrier of X
((k,X,s,t) * s) . (k + 1) is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * s)) . k) + (((k,X,s,t) * s) . (k + 1)) is Element of the carrier of X
((k,X,s,t) . (k + 1)) * s is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * s)) . k) + (((k,X,s,t) . (k + 1)) * s) is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * s)) . k) + ((0. X) * s) is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * s)) . k) + (0. X) is Element of the carrier of X
0 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Partial_Sums (X,((k,X,s,t) * s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,((k,X,s,t) * s))) . (k + 1) is Element of the carrier of X
((Partial_Sums (X,((k,X,s,t) * s))) . (k + 1)) + (((k,X,s,t) * s) . (k + 1)) is Element of the carrier of X
((Partial_Sums (X,((k,X,s,t) * s))) . (k + 1)) + (((k,X,s,t) . (k + 1)) * s) is Element of the carrier of X
((Partial_Sums (X,((k,X,s,t) * s))) . (k + 1)) + (0. X) is Element of the carrier of X
(k,X,s,t) * (s + t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((k,X,s,t) * (s + t)) . p is Element of the carrier of X
(k,X,s,t) . p is Element of the carrier of X
((k,X,s,t) . p) * (s + t) is Element of the carrier of X
((k,X,s,t) . p) * s is Element of the carrier of X
((k,X,s,t) . p) * t is Element of the carrier of X
(((k,X,s,t) . p) * s) + (((k,X,s,t) . p) * t) is Element of the carrier of X
((k,X,s,t) * s) . p is Element of the carrier of X
(((k,X,s,t) * s) . p) + (((k,X,s,t) . p) * t) is Element of the carrier of X
((k,X,s,t) * t) . p is Element of the carrier of X
(((k,X,s,t) * s) . p) + (((k,X,s,t) * t) . p) is Element of the carrier of X
((k,X,s,t) * s) + ((k,X,s,t) * t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(((k,X,s,t) * s) + ((k,X,s,t) * t)) . p is Element of the carrier of X
((s + t) GeoSeq) . k is Element of the carrier of X
(((s + t) GeoSeq) . k) * (s + t) is Element of the carrier of X
(Partial_Sums (k,X,s,t)) * (s + t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((Partial_Sums (k,X,s,t)) * (s + t)) . k is Element of the carrier of X
Partial_Sums ((k,X,s,t) * (s + t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((k,X,s,t) * (s + t))) . k is Element of the carrier of X
(Partial_Sums ((k,X,s,t) * s)) + (Partial_Sums ((k,X,s,t) * t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((Partial_Sums ((k,X,s,t) * s)) + (Partial_Sums ((k,X,s,t) * t))) . k is Element of the carrier of X
((Partial_Sums ((k,X,s,t) * s)) . k) + ((Partial_Sums ((k,X,s,t) * t)) . k) is Element of the carrier of X
(Partial_Sums ((k,X,s,t) * t)) + (Partial_Sums (X,((k,X,s,t) * s))) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((Partial_Sums ((k,X,s,t) * t)) + (Partial_Sums (X,((k,X,s,t) * s)))) . (k + 1) is Element of the carrier of X
0 -' 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 - 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() Element of REAL
(0,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (0,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (0,X,s,t)) . 0 is Element of the carrier of X
(0,X,s,t) . 0 is Element of the carrier of X
s #N 0 is Element of the carrier of X
s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(s GeoSeq) . 0 is Element of the carrier of X
(0) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(0) . 0 is V11() real ext-real Element of REAL
((0) . 0) * (s #N 0) is Element of the carrier of X
t #N 0 is Element of the carrier of X
t GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(t GeoSeq) . 0 is Element of the carrier of X
(((0) . 0) * (s #N 0)) * (t #N 0) is Element of the carrier of X
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
1 / (1 * 1) is V11() real ext-real non negative Element of REAL
(1 / (1 * 1)) * (s #N 0) is Element of the carrier of X
((1 / (1 * 1)) * (s #N 0)) * (t #N 0) is Element of the carrier of X
(s GeoSeq) . 0 is Element of the carrier of X
((s GeoSeq) . 0) * (t #N 0) is Element of the carrier of X
1. X is Element of the carrier of X
(t GeoSeq) . 0 is Element of the carrier of X
(1. X) * ((t GeoSeq) . 0) is Element of the carrier of X
(1. X) * (1. X) is Element of the carrier of X
(s + t) #N 0 is Element of the carrier of X
((s + t) GeoSeq) . 0 is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(t,X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
(t,X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
t ! is V11() real ext-real Element of REAL
1 / (t !) is V11() real ext-real Element of REAL
(1 / (t !)) * (t,X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k ! is V11() real ext-real Element of REAL
t -' k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(t -' k) ! is V11() real ext-real Element of REAL
(k !) * ((t -' k) !) is V11() real ext-real Element of REAL
1 / ((k !) * ((t -' k) !)) is V11() real ext-real Element of REAL
(t !) * 1 is V11() real ext-real Element of REAL
((t !) * 1) / (t !) is V11() real ext-real Element of REAL
(((t !) * 1) / (t !)) / ((k !) * ((t -' k) !)) is V11() real ext-real Element of REAL
(1 / (t !)) * (t !) is V11() real ext-real Element of REAL
((1 / (t !)) * (t !)) / ((k !) * ((t -' k) !)) is V11() real ext-real Element of REAL
(t,X,z,s) . k is Element of the carrier of X
z #N k is Element of the carrier of X
z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(z GeoSeq) . k is Element of the carrier of X
(t) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(t) . k is V11() real ext-real Element of REAL
((t) . k) * (z #N k) is Element of the carrier of X
s #N (t -' k) is Element of the carrier of X
s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(s GeoSeq) . (t -' k) is Element of the carrier of X
(((t) . k) * (z #N k)) * (s #N (t -' k)) is Element of the carrier of X
(1 / ((k !) * ((t -' k) !))) * (z #N k) is Element of the carrier of X
((1 / ((k !) * ((t -' k) !))) * (z #N k)) * (s #N (t -' k)) is Element of the carrier of X
(z #N k) * (s #N (t -' k)) is Element of the carrier of X
(((1 / (t !)) * (t !)) / ((k !) * ((t -' k) !))) * ((z #N k) * (s #N (t -' k))) is Element of the carrier of X
(t !) / ((k !) * ((t -' k) !)) is V11() real ext-real Element of REAL
(1 / (t !)) * ((t !) / ((k !) * ((t -' k) !))) is V11() real ext-real Element of REAL
((1 / (t !)) * ((t !) / ((k !) * ((t -' k) !)))) * ((z #N k) * (s #N (t -' k))) is Element of the carrier of X
((t !) / ((k !) * ((t -' k) !))) * ((z #N k) * (s #N (t -' k))) is Element of the carrier of X
(1 / (t !)) * (((t !) / ((k !) * ((t -' k) !))) * ((z #N k) * (s #N (t -' k)))) is Element of the carrier of X
((t !) / ((k !) * ((t -' k) !))) * (z #N k) is Element of the carrier of X
(((t !) / ((k !) * ((t -' k) !))) * (z #N k)) * (s #N (t -' k)) is Element of the carrier of X
(1 / (t !)) * ((((t !) / ((k !) * ((t -' k) !))) * (z #N k)) * (s #N (t -' k))) is Element of the carrier of X
(t) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(t) . k is V11() real ext-real Element of REAL
((t) . k) * (z #N k) is Element of the carrier of X
(((t) . k) * (z #N k)) * (s #N (t -' k)) is Element of the carrier of X
(1 / (t !)) * ((((t) . k) * (z #N k)) * (s #N (t -' k))) is Element of the carrier of X
(t,X,z,s) . k is Element of the carrier of X
(1 / (t !)) * ((t,X,z,s) . k) is Element of the carrier of X
((1 / (t !)) * (t,X,z,s)) . k is Element of the carrier of X
0. X is V82(X) Element of the carrier of X
(1 / (t !)) * (0. X) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z ! is V11() real ext-real Element of REAL
1 / (z !) is V11() real ext-real Element of REAL
s is Element of the carrier of X
t is Element of the carrier of X
s + t is Element of the carrier of X
(s + t) #N z is Element of the carrier of X
(s + t) GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
((s + t) GeoSeq) . z is Element of the carrier of X
(1 / (z !)) * ((s + t) #N z) is Element of the carrier of X
(z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (z,X,s,t)) . z is Element of the carrier of X
(z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (z,X,s,t)) . z is Element of the carrier of X
(1 / (z !)) * ((Partial_Sums (z,X,s,t)) . z) is Element of the carrier of X
(1 / (z !)) * (Partial_Sums (z,X,s,t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((1 / (z !)) * (Partial_Sums (z,X,s,t))) . z is Element of the carrier of X
(1 / (z !)) * (z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums ((1 / (z !)) * (z,X,s,t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((1 / (z !)) * (z,X,s,t))) . z is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
0. X is V82(X) Element of the carrier of X
the carrier of X is V1() set
(X,(0. X)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Sum (X,(0. X)) is Element of the carrier of X
Partial_Sums (X,(0. X)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,(0. X))) is Element of the carrier of X
1. X is Element of the carrier of X
||.(X,(0. X)).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,(0. X)).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(Partial_Sums ||.(X,(0. X)).||) . z is V11() real ext-real Element of REAL
z + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.(X,(0. X)).||) . (z + 1) is V11() real ext-real Element of REAL
(Partial_Sums ||.(X,(0. X)).||) . z is V11() real ext-real Element of REAL
(Partial_Sums ||.(X,(0. X)).||) . (z + 1) is V11() real ext-real Element of REAL
||.(X,(0. X)).|| . (z + 1) is V11() real ext-real Element of REAL
1 + (||.(X,(0. X)).|| . (z + 1)) is V11() real ext-real Element of REAL
(X,(0. X)) . (z + 1) is Element of the carrier of X
||.((X,(0. X)) . (z + 1)).|| is V11() real ext-real Element of REAL
1 + ||.((X,(0. X)) . (z + 1)).|| is V11() real ext-real Element of REAL
1 / (z + 1) is V11() real ext-real non negative Element of REAL
(1 / (z + 1)) * (0. X) is Element of the carrier of X
(X,(0. X)) . z is Element of the carrier of X
((1 / (z + 1)) * (0. X)) * ((X,(0. X)) . z) is Element of the carrier of X
||.(((1 / (z + 1)) * (0. X)) * ((X,(0. X)) . z)).|| is V11() real ext-real Element of REAL
1 + ||.(((1 / (z + 1)) * (0. X)) * ((X,(0. X)) . z)).|| is V11() real ext-real Element of REAL
(0. X) * ((X,(0. X)) . z) is Element of the carrier of X
||.((0. X) * ((X,(0. X)) . z)).|| is V11() real ext-real Element of REAL
1 + ||.((0. X) * ((X,(0. X)) . z)).|| is V11() real ext-real Element of REAL
||.(0. X).|| is V11() real ext-real Element of REAL
1 + ||.(0. X).|| is V11() real ext-real Element of REAL
1 + 0 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.(X,(0. X)).||) . 0 is V11() real ext-real Element of REAL
||.(X,(0. X)).|| . 0 is V11() real ext-real Element of REAL
(X,(0. X)) . 0 is Element of the carrier of X
||.((X,(0. X)) . 0).|| is V11() real ext-real Element of REAL
||.(1. X).|| is V11() real ext-real Element of REAL
(Partial_Sums ||.(X,(0. X)).||) . 0 is V11() real ext-real Element of REAL
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(Partial_Sums ||.(X,(0. X)).||) . z is V11() real ext-real set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,(0. X))) . z is set
z + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,(0. X))) . (z + 1) is set
(Partial_Sums (X,(0. X))) . z is Element of the carrier of X
(Partial_Sums (X,(0. X))) . (z + 1) is Element of the carrier of X
(X,(0. X)) . (z + 1) is Element of the carrier of X
(1. X) + ((X,(0. X)) . (z + 1)) is Element of the carrier of X
1 / (z + 1) is V11() real ext-real non negative Element of REAL
(1 / (z + 1)) * (0. X) is Element of the carrier of X
(X,(0. X)) . z is Element of the carrier of X
((1 / (z + 1)) * (0. X)) * ((X,(0. X)) . z) is Element of the carrier of X
(1. X) + (((1 / (z + 1)) * (0. X)) * ((X,(0. X)) . z)) is Element of the carrier of X
(0. X) * ((X,(0. X)) . z) is Element of the carrier of X
(1. X) + ((0. X) * ((X,(0. X)) . z)) is Element of the carrier of X
(1. X) + (0. X) is Element of the carrier of X
(Partial_Sums (X,(0. X))) . 0 is Element of the carrier of X
(Partial_Sums (X,(0. X))) . 0 is set
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
||.z.|| is V11() real ext-real Element of REAL
||.z.|| rExpSeq is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z) . s is Element of the carrier of X
||.((X,z) . s).|| is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . s is V11() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
1. X is Element of the carrier of X
z is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
(X,z) . 0 is Element of the carrier of X
s is Element of the carrier of X
(0,X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(0,X,z,s) . 0 is Element of the carrier of X
z #N 0 is Element of the carrier of X
z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(z GeoSeq) . 0 is Element of the carrier of X
1 / (0 !) is V11() real ext-real Element of REAL
(1 / (0 !)) * (z #N 0) is Element of the carrier of X
1 / 1 is V11() real ext-real non negative Element of REAL
(1 / 1) * (1. X) is Element of the carrier of X
0 -' 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(0) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(0) . 0 is V11() real ext-real Element of REAL
((0) . 0) * (z #N 0) is Element of the carrier of X
s #N 0 is Element of the carrier of X
s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(s GeoSeq) . 0 is Element of the carrier of X
(((0) . 0) * (z #N 0)) * (s #N 0) is Element of the carrier of X
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
1 / (1 * 1) is V11() real ext-real non negative Element of REAL
(1 / (1 * 1)) * (z #N 0) is Element of the carrier of X
((1 / (1 * 1)) * (z #N 0)) * (s #N 0) is Element of the carrier of X
(z GeoSeq) . 0 is Element of the carrier of X
((z GeoSeq) . 0) * (s #N 0) is Element of the carrier of X
(s GeoSeq) . 0 is Element of the carrier of X
(1. X) * ((s GeoSeq) . 0) is Element of the carrier of X
(1. X) * (1. X) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((k + 1),X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
((k + 1),X,z,s) . t is Element of the carrier of X
(k,X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(k,X,z,s) . t is Element of the carrier of X
((k + 1),X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((k + 1),X,z,s) . t is Element of the carrier of X
((k,X,z,s) . t) + (((k + 1),X,z,s) . t) is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
(X,z) . t is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
(k + 1) -' t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,s) . ((k + 1) -' t) is Element of the carrier of X
((X,z) . t) * ((X,s) . ((k + 1) -' t)) is Element of the carrier of X
z #N t is Element of the carrier of X
z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(z GeoSeq) . t is Element of the carrier of X
t ! is V11() real ext-real Element of REAL
1 / (t !) is V11() real ext-real Element of REAL
(1 / (t !)) * (z #N t) is Element of the carrier of X
((1 / (t !)) * (z #N t)) * ((X,s) . ((k + 1) -' t)) is Element of the carrier of X
s #N ((k + 1) -' t) is Element of the carrier of X
s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(s GeoSeq) . ((k + 1) -' t) is Element of the carrier of X
((k + 1) -' t) ! is V11() real ext-real Element of REAL
1 / (((k + 1) -' t) !) is V11() real ext-real Element of REAL
(1 / (((k + 1) -' t) !)) * (s #N ((k + 1) -' t)) is Element of the carrier of X
((1 / (t !)) * (z #N t)) * ((1 / (((k + 1) -' t) !)) * (s #N ((k + 1) -' t))) is Element of the carrier of X
(z #N t) * (s #N ((k + 1) -' t)) is Element of the carrier of X
(1 / (t !)) * (1 / (((k + 1) -' t) !)) is V11() real ext-real Element of REAL
((1 / (t !)) * (1 / (((k + 1) -' t) !))) * ((z #N t) * (s #N ((k + 1) -' t))) is Element of the carrier of X
(t !) * (((k + 1) -' t) !) is V11() real ext-real Element of REAL
1 / ((t !) * (((k + 1) -' t) !)) is V11() real ext-real Element of REAL
(1 / ((t !) * (((k + 1) -' t) !))) * ((z #N t) * (s #N ((k + 1) -' t))) is Element of the carrier of X
((k + 1)) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((k + 1)) . t is V11() real ext-real Element of REAL
(((k + 1)) . t) * ((z #N t) * (s #N ((k + 1) -' t))) is Element of the carrier of X
(((k + 1)) . t) * (z #N t) is Element of the carrier of X
((((k + 1)) . t) * (z #N t)) * (s #N ((k + 1) -' t)) is Element of the carrier of X
(k + 1) - t is V11() real ext-real Element of REAL
k - t is V11() real ext-real Element of REAL
(k - t) + 1 is V11() real ext-real Element of REAL
k -' t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k -' t) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Partial_Sums (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,s)) . ((k -' t) + 1) is Element of the carrier of X
((X,z) . t) * ((Partial_Sums (X,s)) . ((k -' t) + 1)) is Element of the carrier of X
(Partial_Sums (X,s)) . (k -' t) is Element of the carrier of X
((Partial_Sums (X,s)) . (k -' t)) + ((X,s) . ((k + 1) -' t)) is Element of the carrier of X
((X,z) . t) * (((Partial_Sums (X,s)) . (k -' t)) + ((X,s) . ((k + 1) -' t))) is Element of the carrier of X
((X,z) . t) * ((Partial_Sums (X,s)) . (k -' t)) is Element of the carrier of X
(((X,z) . t) * ((Partial_Sums (X,s)) . (k -' t))) + (((X,z) . t) * ((X,s) . ((k + 1) -' t))) is Element of the carrier of X
((k,X,z,s) . t) + (((X,z) . t) * ((X,s) . ((k + 1) -' t))) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((t + 1),X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Partial_Sums ((t + 1),X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((t + 1),X,z,s)) . t is Element of the carrier of X
(t,X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (t,X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (t,X,z,s)) . t is Element of the carrier of X
((t + 1),X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums ((t + 1),X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((t + 1),X,z,s)) . t is Element of the carrier of X
((Partial_Sums (t,X,z,s)) . t) + ((Partial_Sums ((t + 1),X,z,s)) . t) is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((t + 1),X,z,s) . k is Element of the carrier of X
(t,X,z,s) . k is Element of the carrier of X
((t + 1),X,z,s) . k is Element of the carrier of X
((t,X,z,s) . k) + (((t + 1),X,z,s) . k) is Element of the carrier of X
(t,X,z,s) + ((t + 1),X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((t,X,z,s) + ((t + 1),X,z,s)) . k is Element of the carrier of X
Partial_Sums ((t,X,z,s) + ((t + 1),X,z,s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((t,X,z,s) + ((t + 1),X,z,s))) . t is Element of the carrier of X
(Partial_Sums (t,X,z,s)) + (Partial_Sums ((t + 1),X,z,s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((Partial_Sums (t,X,z,s)) + (Partial_Sums ((t + 1),X,z,s))) . t is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
s is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z) . t is Element of the carrier of X
(t,X,z,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(t,X,z,s) . t is Element of the carrier of X
t - t is V11() real ext-real Element of REAL
t -' t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(t -' t) ! is V11() real ext-real Element of REAL
z #N t is Element of the carrier of X
z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(z GeoSeq) . t is Element of the carrier of X
(t) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(t) . t is V11() real ext-real Element of REAL
((t) . t) * (z #N t) is Element of the carrier of X
s #N 0 is Element of the carrier of X
s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(s GeoSeq) . 0 is Element of the carrier of X
(((t) . t) * (z #N t)) * (s #N 0) is Element of the carrier of X
1. X is Element of the carrier of X
(((t) . t) * (z #N t)) * (1. X) is Element of the carrier of X
t ! is V11() real ext-real Element of REAL
(t !) * 1 is V11() real ext-real Element of REAL
1 / ((t !) * 1) is V11() real ext-real Element of REAL
(1 / ((t !) * 1)) * (z #N t) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of X
t is Element of the carrier of X
s + t is Element of the carrier of X
(X,(s + t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Partial_Sums (X,(s + t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,(s + t))) . z is Element of the carrier of X
(z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (z,X,s,t)) . z is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,(s + t))) . k is Element of the carrier of X
(k,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (k,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (k,X,s,t)) . k is Element of the carrier of X
k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,(s + t))) . (k + 1) is Element of the carrier of X
((k + 1),X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums ((k + 1),X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((k + 1),X,s,t)) . (k + 1) is Element of the carrier of X
(k + 1) -' (k + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((k + 1),X,s,t) . (k + 1) is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
(X,s) . (k + 1) is Element of the carrier of X
(X,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,t)) . 0 is Element of the carrier of X
((X,s) . (k + 1)) * ((Partial_Sums (X,t)) . 0) is Element of the carrier of X
(X,t) . 0 is Element of the carrier of X
((X,s) . (k + 1)) * ((X,t) . 0) is Element of the carrier of X
1. X is Element of the carrier of X
((X,s) . (k + 1)) * (1. X) is Element of the carrier of X
((k + 1),X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((k + 1),X,s,t) . (k + 1) is Element of the carrier of X
Partial_Sums ((k + 1),X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((k + 1),X,s,t)) . k is Element of the carrier of X
((Partial_Sums ((k + 1),X,s,t)) . k) + (((k + 1),X,s,t) . (k + 1)) is Element of the carrier of X
(Partial_Sums ((k + 1),X,s,t)) . (k + 1) is Element of the carrier of X
(s + t) #N (k + 1) is Element of the carrier of X
(s + t) GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((s + t) GeoSeq) . (k + 1) is Element of the carrier of X
(k + 1) ! is V11() real ext-real Element of REAL
1 / ((k + 1) !) is V11() real ext-real Element of REAL
(1 / ((k + 1) !)) * ((s + t) #N (k + 1)) is Element of the carrier of X
(Partial_Sums ((k + 1),X,s,t)) . k is Element of the carrier of X
((Partial_Sums ((k + 1),X,s,t)) . k) + (((k + 1),X,s,t) . (k + 1)) is Element of the carrier of X
((Partial_Sums (k,X,s,t)) . k) + ((Partial_Sums ((k + 1),X,s,t)) . k) is Element of the carrier of X
(((Partial_Sums (k,X,s,t)) . k) + ((Partial_Sums ((k + 1),X,s,t)) . k)) + (((k + 1),X,s,t) . (k + 1)) is Element of the carrier of X
((Partial_Sums (X,(s + t))) . k) + (((Partial_Sums ((k + 1),X,s,t)) . k) + (((k + 1),X,s,t) . (k + 1))) is Element of the carrier of X
(X,(s + t)) . (k + 1) is Element of the carrier of X
((Partial_Sums (X,(s + t))) . k) + ((X,(s + t)) . (k + 1)) is Element of the carrier of X
(Partial_Sums (X,(s + t))) . 0 is Element of the carrier of X
(X,(s + t)) . 0 is Element of the carrier of X
1. X is Element of the carrier of X
0 -' 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(0,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (0,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (0,X,s,t)) . 0 is Element of the carrier of X
(0,X,s,t) . 0 is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
(X,s) . 0 is Element of the carrier of X
(X,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,t)) . 0 is Element of the carrier of X
((X,s) . 0) * ((Partial_Sums (X,t)) . 0) is Element of the carrier of X
(X,t) . 0 is Element of the carrier of X
((X,s) . 0) * ((X,t) . 0) is Element of the carrier of X
(1. X) * ((X,t) . 0) is Element of the carrier of X
(1. X) * (1. X) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Partial_Sums (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,s)) . z is Element of the carrier of X
t is Element of the carrier of X
(X,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,t)) . z is Element of the carrier of X
((Partial_Sums (X,s)) . z) * ((Partial_Sums (X,t)) . z) is Element of the carrier of X
s + t is Element of the carrier of X
(X,(s + t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,(s + t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,(s + t))) . z is Element of the carrier of X
(((Partial_Sums (X,s)) . z) * ((Partial_Sums (X,t)) . z)) - ((Partial_Sums (X,(s + t))) . z) is Element of the carrier of X
(X,s,t,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,s,t,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,s,t,z)) . z is Element of the carrier of X
(z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (z,X,s,t)) . z is Element of the carrier of X
(((Partial_Sums (X,s)) . z) * ((Partial_Sums (X,t)) . z)) - ((Partial_Sums (z,X,s,t)) . z) is Element of the carrier of X
(Partial_Sums (X,s)) * ((Partial_Sums (X,t)) . z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((Partial_Sums (X,s)) * ((Partial_Sums (X,t)) . z)) . z is Element of the carrier of X
(((Partial_Sums (X,s)) * ((Partial_Sums (X,t)) . z)) . z) - ((Partial_Sums (z,X,s,t)) . z) is Element of the carrier of X
(X,s) * ((Partial_Sums (X,t)) . z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums ((X,s) * ((Partial_Sums (X,t)) . z)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums ((X,s) * ((Partial_Sums (X,t)) . z))) . z is Element of the carrier of X
((Partial_Sums ((X,s) * ((Partial_Sums (X,t)) . z))) . z) - ((Partial_Sums (z,X,s,t)) . z) is Element of the carrier of X
(Partial_Sums ((X,s) * ((Partial_Sums (X,t)) . z))) - (Partial_Sums (z,X,s,t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((Partial_Sums ((X,s) * ((Partial_Sums (X,t)) . z))) - (Partial_Sums (z,X,s,t))) . z is Element of the carrier of X
((X,s) * ((Partial_Sums (X,t)) . z)) - (z,X,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (((X,s) * ((Partial_Sums (X,t)) . z)) - (z,X,s,t)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (((X,s) * ((Partial_Sums (X,t)) . z)) - (z,X,s,t))) . z is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(((X,s) * ((Partial_Sums (X,t)) . z)) - (z,X,s,t)) . k is Element of the carrier of X
(X,s,t,z) . k is Element of the carrier of X
((X,s) * ((Partial_Sums (X,t)) . z)) . k is Element of the carrier of X
(z,X,s,t) . k is Element of the carrier of X
(((X,s) * ((Partial_Sums (X,t)) . z)) . k) - ((z,X,s,t) . k) is Element of the carrier of X
(X,s) . k is Element of the carrier of X
((X,s) . k) * ((Partial_Sums (X,t)) . z) is Element of the carrier of X
(((X,s) . k) * ((Partial_Sums (X,t)) . z)) - ((z,X,s,t) . k) is Element of the carrier of X
z -' k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,t)) . (z -' k) is Element of the carrier of X
((X,s) . k) * ((Partial_Sums (X,t)) . (z -' k)) is Element of the carrier of X
(((X,s) . k) * ((Partial_Sums (X,t)) . z)) - (((X,s) . k) * ((Partial_Sums (X,t)) . (z -' k))) is Element of the carrier of X
((Partial_Sums (X,t)) . z) - ((Partial_Sums (X,t)) . (z -' k)) is Element of the carrier of X
((X,s) . k) * (((Partial_Sums (X,t)) . z) - ((Partial_Sums (X,t)) . (z -' k))) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
||.z.|| is V11() real ext-real Element of REAL
||.z.|| rExpSeq is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(||.z.|| rExpSeq) . s is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.z.|| |^ t is V11() real ext-real Element of REAL
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.z.|| |^ (t + 1) is V11() real ext-real Element of REAL
(||.z.|| |^ t) * ||.z.|| is V11() real ext-real Element of REAL
||.z.|| |^ 0 is V11() real ext-real Element of REAL
||.z.|| |^ s is V11() real ext-real Element of REAL
s ! is V11() real ext-real Element of REAL
(||.z.|| |^ s) / (s !) is V11() real ext-real Element of REAL
(s !) " is V11() real ext-real Element of REAL
(||.z.|| |^ s) * ((s !) ") is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Partial_Sums (X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.z.|| is V11() real ext-real Element of REAL
||.z.|| rExpSeq is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums (||.z.|| rExpSeq) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Sum (||.z.|| rExpSeq) is V11() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,z)) . s is Element of the carrier of X
||.((Partial_Sums (X,z)) . s).|| is V11() real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . s is V11() real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . 0 is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . 0 is V11() real ext-real Element of REAL
||.z.|| |^ 0 is V11() real ext-real Element of REAL
(||.z.|| |^ 0) / (0 !) is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,z)) . t is Element of the carrier of X
||.((Partial_Sums (X,z)) . t).|| is V11() real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . t is V11() real ext-real Element of REAL
t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,z)) . (t + 1) is Element of the carrier of X
||.((Partial_Sums (X,z)) . (t + 1)).|| is V11() real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . (t + 1) is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . (t + 1) is V11() real ext-real Element of REAL
||.((Partial_Sums (X,z)) . t).|| + ((||.z.|| rExpSeq) . (t + 1)) is V11() real ext-real Element of REAL
((Partial_Sums (||.z.|| rExpSeq)) . t) + ((||.z.|| rExpSeq) . (t + 1)) is V11() real ext-real Element of REAL
(X,z) . (t + 1) is Element of the carrier of X
((Partial_Sums (X,z)) . t) + ((X,z) . (t + 1)) is Element of the carrier of X
||.(((Partial_Sums (X,z)) . t) + ((X,z) . (t + 1))).|| is V11() real ext-real Element of REAL
||.((X,z) . (t + 1)).|| is V11() real ext-real Element of REAL
||.((Partial_Sums (X,z)) . t).|| + ||.((X,z) . (t + 1)).|| is V11() real ext-real Element of REAL
(Partial_Sums (X,z)) . 0 is Element of the carrier of X
||.((Partial_Sums (X,z)) . 0).|| is V11() real ext-real Element of REAL
(X,z) . 0 is Element of the carrier of X
||.((X,z) . 0).|| is V11() real ext-real Element of REAL
z #N 0 is Element of the carrier of X
z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(z GeoSeq) . 0 is Element of the carrier of X
1 / (0 !) is V11() real ext-real Element of REAL
(1 / (0 !)) * (z #N 0) is Element of the carrier of X
||.((1 / (0 !)) * (z #N 0)).|| is V11() real ext-real Element of REAL
1. X is Element of the carrier of X
1 / 1 is V11() real ext-real non negative Element of REAL
(1 / 1) * (1. X) is Element of the carrier of X
||.((1 / 1) * (1. X)).|| is V11() real ext-real Element of REAL
||.(1. X).|| is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(||.z.|| rExpSeq) . t is V11() real ext-real Element of REAL
lim (Partial_Sums (||.z.|| rExpSeq)) is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (||.z.|| rExpSeq)) . t is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
||.z.|| is V11() real ext-real Element of REAL
||.z.|| rExpSeq is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Sum (||.z.|| rExpSeq) is V11() real ext-real Element of REAL
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Partial_Sums (X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,z)) . 0 is Element of the carrier of X
||.((Partial_Sums (X,z)) . 0).|| is V11() real ext-real Element of REAL
(X,z) . 0 is Element of the carrier of X
||.((X,z) . 0).|| is V11() real ext-real Element of REAL
1. X is Element of the carrier of X
||.(1. X).|| is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
||.z.|| is V11() real ext-real Element of REAL
||.z.|| rExpSeq is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums (||.z.|| rExpSeq) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (||.z.|| rExpSeq)) . s is V11() real ext-real Element of REAL
abs ((Partial_Sums (||.z.|| rExpSeq)) . s) is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (||.z.|| rExpSeq)) . t is V11() real ext-real Element of REAL
((Partial_Sums (||.z.|| rExpSeq)) . t) - ((Partial_Sums (||.z.|| rExpSeq)) . s) is V11() real ext-real Element of REAL
abs (((Partial_Sums (||.z.|| rExpSeq)) . t) - ((Partial_Sums (||.z.|| rExpSeq)) . s)) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(||.z.|| rExpSeq) . k is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z,s,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
||.(X,z,s,t).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,t).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.(X,z,s,t).||) . k is V11() real ext-real Element of REAL
abs ((Partial_Sums ||.(X,z,s,t).||) . k) is V11() real ext-real Element of REAL
(Partial_Sums ||.(X,z,s,t).||) . 0 is V11() real ext-real Element of REAL
||.(X,z,s,t).|| . 0 is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X,z,s,t).|| . p is V11() real ext-real Element of REAL
(X,z,s,t) . p is Element of the carrier of X
||.((X,z,s,t) . p).|| is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is Element of the carrier of X
t is V11() real ext-real set
k is V11() real ext-real Element of REAL
||.z.|| is V11() real ext-real Element of REAL
||.z.|| rExpSeq is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Sum (||.z.|| rExpSeq) is V11() real ext-real Element of REAL
4 * (Sum (||.z.|| rExpSeq)) is V11() real ext-real Element of REAL
k / (4 * (Sum (||.z.|| rExpSeq))) is V11() real ext-real Element of REAL
||.s.|| is V11() real ext-real Element of REAL
||.s.|| rExpSeq is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Sum (||.s.|| rExpSeq) is V11() real ext-real Element of REAL
4 * (Sum (||.s.|| rExpSeq)) is V11() real ext-real Element of REAL
k / (4 * (Sum (||.s.|| rExpSeq))) is V11() real ext-real Element of REAL
min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq))))) is V11() real ext-real Element of REAL
0 * (Sum (||.z.|| rExpSeq)) is V11() real ext-real Element of REAL
t / (4 * (Sum (||.z.|| rExpSeq))) is V11() real ext-real Element of REAL
0 / (4 * (Sum (||.z.|| rExpSeq))) is V11() real ext-real Element of REAL
0 * (Sum (||.s.|| rExpSeq)) is V11() real ext-real Element of REAL
t / (4 * (Sum (||.s.|| rExpSeq))) is V11() real ext-real Element of REAL
0 / (4 * (Sum (||.s.|| rExpSeq))) is V11() real ext-real Element of REAL
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Partial_Sums (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Partial_Sums (||.z.|| rExpSeq) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(n + n) + (n + n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
(X,z) . l is Element of the carrier of X
(Partial_Sums (X,s)) . l is Element of the carrier of X
l -' l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,s)) . (l -' l) is Element of the carrier of X
((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l)) is Element of the carrier of X
((X,z) . l) * (((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))) is Element of the carrier of X
||.(((X,z) . l) * (((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l)))).|| is V11() real ext-real Element of REAL
||.((X,z) . l).|| is V11() real ext-real Element of REAL
||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is V11() real ext-real Element of REAL
||.((X,z) . l).|| * ||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . l is V11() real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is V11() real ext-real Element of REAL
(X,z,s,l) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.(X,z,s,l).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.(X,z,s,l).|| . l is V11() real ext-real Element of REAL
(X,z,s,l) . l is Element of the carrier of X
||.((X,z,s,l) . l).|| is V11() real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X,z,s,l).|| . l is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . l is V11() real ext-real Element of REAL
l -' l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,s)) . (l -' l) is Element of the carrier of X
((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l)) is Element of the carrier of X
||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is V11() real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,s)) . k is Element of the carrier of X
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k -' l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,s)) . (k -' l) is Element of the carrier of X
((Partial_Sums (X,s)) . k) - ((Partial_Sums (X,s)) . (k -' l)) is Element of the carrier of X
||.(((Partial_Sums (X,s)) . k) - ((Partial_Sums (X,s)) . (k -' l))).|| is V11() real ext-real Element of REAL
||.((Partial_Sums (X,s)) . k).|| is V11() real ext-real Element of REAL
||.((Partial_Sums (X,s)) . (k -' l)).|| is V11() real ext-real Element of REAL
||.((Partial_Sums (X,s)) . k).|| + ||.((Partial_Sums (X,s)) . (k -' l)).|| is V11() real ext-real Element of REAL
(Sum (||.s.|| rExpSeq)) + ||.((Partial_Sums (X,s)) . (k -' l)).|| is V11() real ext-real Element of REAL
(Sum (||.s.|| rExpSeq)) + (Sum (||.s.|| rExpSeq)) is V11() real ext-real Element of REAL
2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
2 * (Sum (||.s.|| rExpSeq)) is V11() real ext-real Element of REAL
(X,z,s,k) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.(X,z,s,k).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.(X,z,s,k).|| . l is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . l is V11() real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (X,s)) . k) - ((Partial_Sums (X,s)) . (k -' l))).|| is V11() real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * (2 * (Sum (||.s.|| rExpSeq))) is V11() real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X,z,s,k).|| . l is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . l is V11() real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * (2 * (Sum (||.s.|| rExpSeq))) is V11() real ext-real Element of REAL
t / 4 is V11() real ext-real Element of REAL
(t / 4) + (t / 4) is V11() real ext-real Element of REAL
0 + (t / 4) is V11() real ext-real Element of REAL
(Sum (||.z.|| rExpSeq)) * (t / (4 * (Sum (||.z.|| rExpSeq)))) is V11() real ext-real Element of REAL
(4 * (Sum (||.z.|| rExpSeq))) " is V11() real ext-real Element of REAL
t * ((4 * (Sum (||.z.|| rExpSeq))) ") is V11() real ext-real Element of REAL
(Sum (||.z.|| rExpSeq)) * (t * ((4 * (Sum (||.z.|| rExpSeq))) ")) is V11() real ext-real Element of REAL
(Sum (||.z.|| rExpSeq)) * t is V11() real ext-real Element of REAL
((Sum (||.z.|| rExpSeq)) * t) * ((4 * (Sum (||.z.|| rExpSeq))) ") is V11() real ext-real Element of REAL
((Sum (||.z.|| rExpSeq)) * t) / (4 * (Sum (||.z.|| rExpSeq))) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 + (n + n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k -' (n + n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - (n + n) is V11() real ext-real Element of REAL
(k -' (n + n)) + (n + n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(||.z.|| rExpSeq) . l is V11() real ext-real Element of REAL
((n + n) + (n + n)) - (n + n) is V11() real ext-real Element of REAL
((n + n) + (n + n)) - l is V11() real ext-real Element of REAL
(X,z,s,k) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.(X,z,s,k).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.(X,z,s,k).|| . l is V11() real ext-real Element of REAL
(Partial_Sums (X,s)) . k is Element of the carrier of X
k -' l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,s)) . (k -' l) is Element of the carrier of X
((Partial_Sums (X,s)) . k) - ((Partial_Sums (X,s)) . (k -' l)) is Element of the carrier of X
||.(((Partial_Sums (X,s)) . k) - ((Partial_Sums (X,s)) . (k -' l))).|| is V11() real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (X,s)) . k) - ((Partial_Sums (X,s)) . (k -' l))).|| is V11() real ext-real Element of REAL
n4 - l is V11() real ext-real Element of REAL
k - l is V11() real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * (min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) is V11() real ext-real Element of REAL
(min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) is V11() real ext-real Element of REAL
Partial_Sums ||.(X,z,s,k).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,k).||) . (n + n) is V11() real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . (n + n) is V11() real ext-real Element of REAL
((Partial_Sums (||.z.|| rExpSeq)) . (n + n)) * (min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) is V11() real ext-real Element of REAL
n + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (||.z.|| rExpSeq)) . k is V11() real ext-real Element of REAL
((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n + n)) is V11() real ext-real Element of REAL
abs (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n + n))) is V11() real ext-real Element of REAL
(((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n + n))) * (2 * (Sum (||.s.|| rExpSeq))) is V11() real ext-real Element of REAL
(min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) * (2 * (Sum (||.s.|| rExpSeq))) is V11() real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X,z,s,k).|| . l is V11() real ext-real Element of REAL
(||.z.|| rExpSeq) . l is V11() real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * ((||.z.|| rExpSeq) . l) is V11() real ext-real Element of REAL
(Partial_Sums ||.(X,z,s,k).||) . k is V11() real ext-real Element of REAL
((Partial_Sums ||.(X,z,s,k).||) . k) - ((Partial_Sums ||.(X,z,s,k).||) . (n + n)) is V11() real ext-real Element of REAL
(Sum (||.z.|| rExpSeq)) * (min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) is V11() real ext-real Element of REAL
t / 2 is V11() real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * (min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) is V11() real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * (t / (4 * (Sum (||.s.|| rExpSeq)))) is V11() real ext-real Element of REAL
(4 * (Sum (||.s.|| rExpSeq))) " is V11() real ext-real Element of REAL
t * ((4 * (Sum (||.s.|| rExpSeq))) ") is V11() real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * (t * ((4 * (Sum (||.s.|| rExpSeq))) ")) is V11() real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * t is V11() real ext-real Element of REAL
((2 * (Sum (||.s.|| rExpSeq))) * t) * ((4 * (Sum (||.s.|| rExpSeq))) ") is V11() real ext-real Element of REAL
2 * t is V11() real ext-real Element of REAL
(2 * t) * (Sum (||.s.|| rExpSeq)) is V11() real ext-real Element of REAL
((2 * t) * (Sum (||.s.|| rExpSeq))) / (4 * (Sum (||.s.|| rExpSeq))) is V11() real ext-real Element of REAL
(2 * t) / 4 is V11() real ext-real Element of REAL
(t / 2) + (t / 2) is V11() real ext-real Element of REAL
(((Partial_Sums ||.(X,z,s,k).||) . k) - ((Partial_Sums ||.(X,z,s,k).||) . (n + n))) + ((Partial_Sums ||.(X,z,s,k).||) . (n + n)) is V11() real ext-real Element of REAL
abs ((Partial_Sums ||.(X,z,s,k).||) . k) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z,s,k) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.(X,z,s,k).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,k).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,k).||) . k is V11() real ext-real Element of REAL
abs ((Partial_Sums ||.(X,z,s,k).||) . k) is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
0. X is V82(X) Element of the carrier of X
z is Element of the carrier of X
s is Element of the carrier of X
t is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
t is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim k is Element of the carrier of X
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . p is Element of the carrier of X
||.(k . p).|| is V11() real ext-real Element of REAL
(X,z,s,p) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,z,s,p) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,z,s,p)) . p is Element of the carrier of X
||.((Partial_Sums (X,z,s,p)) . p).|| is V11() real ext-real Element of REAL
||.(X,z,s,p).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,p).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,p).||) . p is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k . p is Element of the carrier of X
||.(k . p).|| is V11() real ext-real Element of REAL
(X,z,s,p) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.(X,z,s,p).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,p).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,p).||) . p is V11() real ext-real Element of REAL
t . p is V11() real ext-real Element of REAL
p is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t . k is V11() real ext-real Element of REAL
(t . k) - 0 is V11() real ext-real Element of REAL
abs ((t . k) - 0) is V11() real ext-real Element of REAL
(X,z,s,k) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.(X,z,s,k).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,k).|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,k).||) . k is V11() real ext-real Element of REAL
abs ((Partial_Sums ||.(X,z,s,k).||) . k) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t . k is V11() real ext-real Element of REAL
(t . k) - 0 is V11() real ext-real Element of REAL
abs ((t . k) - 0) is V11() real ext-real Element of REAL
lim t is V11() real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Sum (X,z) is Element of the carrier of X
Partial_Sums (X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,z)) is Element of the carrier of X
s is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Sum (X,s) is Element of the carrier of X
Partial_Sums (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,s)) is Element of the carrier of X
(Sum (X,z)) * (Sum (X,s)) is Element of the carrier of X
z + s is Element of the carrier of X
(X,(z + s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Sum (X,(z + s)) is Element of the carrier of X
Partial_Sums (X,(z + s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,(z + s))) is Element of the carrier of X
t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t . k is Element of the carrier of X
(X,z,s,k) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Partial_Sums (X,z,s,k) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(Partial_Sums (X,z,s,k)) . k is Element of the carrier of X
(Partial_Sums (X,z)) . k is Element of the carrier of X
(Partial_Sums (X,s)) . k is Element of the carrier of X
((Partial_Sums (X,z)) . k) * ((Partial_Sums (X,s)) . k) is Element of the carrier of X
(Partial_Sums (X,(z + s))) . k is Element of the carrier of X
(((Partial_Sums (X,z)) . k) * ((Partial_Sums (X,s)) . k)) - ((Partial_Sums (X,(z + s))) . k) is Element of the carrier of X
(Partial_Sums (X,z)) * (Partial_Sums (X,s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((Partial_Sums (X,z)) * (Partial_Sums (X,s))) . k is Element of the carrier of X
(((Partial_Sums (X,z)) * (Partial_Sums (X,s))) . k) - ((Partial_Sums (X,(z + s))) . k) is Element of the carrier of X
((Partial_Sums (X,z)) * (Partial_Sums (X,s))) - (Partial_Sums (X,(z + s))) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(((Partial_Sums (X,z)) * (Partial_Sums (X,s))) - (Partial_Sums (X,(z + s)))) . k is Element of the carrier of X
lim t is Element of the carrier of X
0. X is V82(X) Element of the carrier of X
lim ((Partial_Sums (X,z)) * (Partial_Sums (X,s))) is Element of the carrier of X
(lim (Partial_Sums (X,z))) * (lim (Partial_Sums (X,s))) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
z is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
z is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
s is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
t is Element of the carrier of X
z . t is Element of the carrier of X
s . t is Element of the carrier of X
(X,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Sum (X,t) is Element of the carrier of X
Partial_Sums (X,t) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,t)) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
(X) is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
z is Element of the carrier of X
(X) . z is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
(X,z) is Element of the carrier of X
(X) is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
(X) . z is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Sum (X,z) is Element of the carrier of X
Partial_Sums (X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,z)) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
(X,z) is Element of the carrier of X
(X) is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
(X) . z is Element of the carrier of X
s is Element of the carrier of X
z + s is Element of the carrier of X
(X,(z + s)) is Element of the carrier of X
(X) . (z + s) is Element of the carrier of X
(X,s) is Element of the carrier of X
(X) . s is Element of the carrier of X
(X,z) * (X,s) is Element of the carrier of X
s + z is Element of the carrier of X
(X,(s + z)) is Element of the carrier of X
(X) . (s + z) is Element of the carrier of X
(X,s) * (X,z) is Element of the carrier of X
(X,(s + z)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Sum (X,(s + z)) is Element of the carrier of X
Partial_Sums (X,(s + z)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,(s + z))) is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Sum (X,s) is Element of the carrier of X
Partial_Sums (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,s)) is Element of the carrier of X
(X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Sum (X,z) is Element of the carrier of X
Partial_Sums (X,z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,z)) is Element of the carrier of X
(Sum (X,s)) * (Sum (X,z)) is Element of the carrier of X
(X,s) * (Sum (X,z)) is Element of the carrier of X
(X,(z + s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
Sum (X,(z + s)) is Element of the carrier of X
Partial_Sums (X,(z + s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,(z + s))) is Element of the carrier of X
(Sum (X,z)) * (Sum (X,s)) is Element of the carrier of X
(X,z) * (Sum (X,s)) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is Element of the carrier of X
(X,s) is Element of the carrier of X
(X) is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
(X) . s is Element of the carrier of X
z * (X,s) is Element of the carrier of X
(X,s) * z is Element of the carrier of X
(X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z * (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(z * (X,s)) . t is Element of the carrier of X
(X,s) . t is Element of the carrier of X
z * ((X,s) . t) is Element of the carrier of X
s #N t is Element of the carrier of X
s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(s GeoSeq) . t is Element of the carrier of X
t ! is V11() real ext-real Element of REAL
1 / (t !) is V11() real ext-real Element of REAL
(1 / (t !)) * (s #N t) is Element of the carrier of X
z * ((1 / (t !)) * (s #N t)) is Element of the carrier of X
z * (s #N t) is Element of the carrier of X
(1 / (t !)) * (z * (s #N t)) is Element of the carrier of X
(s #N t) * z is Element of the carrier of X
(1 / (t !)) * ((s #N t) * z) is Element of the carrier of X
((1 / (t !)) * (s #N t)) * z is Element of the carrier of X
((X,s) . t) * z is Element of the carrier of X
(X,s) * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((X,s) * z) . t is Element of the carrier of X
Partial_Sums (X,s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Sum (X,s) is Element of the carrier of X
lim (Partial_Sums (X,s)) is Element of the carrier of X
z * (Sum (X,s)) is Element of the carrier of X
z * (Partial_Sums (X,s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (z * (Partial_Sums (X,s))) is Element of the carrier of X
Partial_Sums (z * (X,s)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (z * (X,s))) is Element of the carrier of X
(Partial_Sums (X,s)) * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim ((Partial_Sums (X,s)) * z) is Element of the carrier of X
(Sum (X,s)) * z is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
0. X is V82(X) Element of the carrier of X
the carrier of X is V1() set
(X,(0. X)) is Element of the carrier of X
(X) is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
(X) . (0. X) is Element of the carrier of X
1. X is Element of the carrier of X
(X,(0. X)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) convergent summable norm_summable Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
Sum (X,(0. X)) is Element of the carrier of X
Partial_Sums (X,(0. X)) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Partial_Sums (X,(0. X))) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
1. X is Element of the carrier of X
z is Element of the carrier of X
(X,z) is Element of the carrier of X
(X) is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
(X) . z is Element of the carrier of X
- z is Element of the carrier of X
(X,(- z)) is Element of the carrier of X
(X) . (- z) is Element of the carrier of X
(X,z) * (X,(- z)) is Element of the carrier of X
(X,(- z)) * (X,z) is Element of the carrier of X
z * (- z) is Element of the carrier of X
(- 1) * z is Element of the carrier of X
z * ((- 1) * z) is Element of the carrier of X
z * z is Element of the carrier of X
(- 1) * (z * z) is Element of the carrier of X
((- 1) * z) * z is Element of the carrier of X
(- z) * z is Element of the carrier of X
z + (- z) is Element of the carrier of X
(X,(z + (- z))) is Element of the carrier of X
(X) . (z + (- z)) is Element of the carrier of X
0. X is V82(X) Element of the carrier of X
(X,(0. X)) is Element of the carrier of X
(X) . (0. X) is Element of the carrier of X
(- z) + z is Element of the carrier of X
(X,((- z) + z)) is Element of the carrier of X
(X) . ((- z) + z) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
(X,z) is Element of the carrier of X
(X) is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
(X) . z is Element of the carrier of X
/ (X,z) is Element of the carrier of X
- z is Element of the carrier of X
(X,(- z)) is Element of the carrier of X
(X) . (- z) is Element of the carrier of X
/ (X,(- z)) is Element of the carrier of X
(X,(- z)) * (X,z) is Element of the carrier of X
1. X is Element of the carrier of X
(X,z) * (X,(- z)) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is V11() real ext-real Element of REAL
s * z is Element of the carrier of X
t is V11() real ext-real Element of REAL
t * z is Element of the carrier of X
(s * z) * (t * z) is Element of the carrier of X
z * z is Element of the carrier of X
s * t is V11() real ext-real Element of REAL
(s * t) * (z * z) is Element of the carrier of X
(t * z) * (s * z) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr
the carrier of X is V1() set
z is Element of the carrier of X
s is V11() real ext-real Element of REAL
s * z is Element of the carrier of X
(X,(s * z)) is Element of the carrier of X
(X) is V1() Relation-like the carrier of X -defined the carrier of X -valued Function-like V26( the carrier of X) V30( the carrier of X, the carrier of X) Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
(X) . (s * z) is Element of the carrier of X
t is V11() real ext-real Element of REAL
t * z is Element of the carrier of X
(X,(t * z)) is Element of the carrier of X
(X) . (t * z) is Element of the carrier of X
(X,(s * z)) * (X,(t * z)) is Element of the carrier of X
s + t is V11() real ext-real Element of REAL
(s + t) * z is Element of the carrier of X
(X,((s + t) * z)) is Element of the carrier of X
(X) . ((s + t) * z) is Element of the carrier of X
(X,(t * z)) * (X,(s * z)) is Element of the carrier of X
t + s is V11() real ext-real Element of REAL
(t + s) * z is Element of the carrier of X
(X,((t + s) * z)) is Element of the carrier of X
(X) . ((t + s) * z) is Element of the carrier of X
(s * z) + (t * z) is Element of the carrier of X
(X,((s * z) + (t * z))) is Element of the carrier of X
(X) . ((s * z) + (t * z)) is Element of the carrier of X
(t * z) + (s * z) is Element of the carrier of X
(X,((t * z) + (s * z))) is Element of the carrier of X
(X) . ((t * z) + (s * z)) is Element of the carrier of X