:: CLOPBAN4 semantic presentation

REAL is non zero V47() V59() V60() V61() V65() set
NAT is non zero epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non zero V47() V59() V65() set
omega is non zero epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() set
K6(omega) is set
K6(NAT) is set
RAT is non zero V47() V59() V60() V61() V62() V65() set
INT is non zero V47() V59() V60() V61() V62() V63() V65() set
K7(NAT,REAL) is V33() V34() V35() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is V33() set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is V33() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(REAL,REAL) is V33() V34() V35() set
K6(K7(REAL,REAL)) is set
K471() is non zero set
K7(K471(),K471()) is set
K7(K7(K471(),K471()),K471()) is set
K6(K7(K7(K471(),K471()),K471())) is set
K7(COMPLEX,K471()) is set
K7(K7(COMPLEX,K471()),K471()) is set
K6(K7(K7(COMPLEX,K471()),K471())) is set
K477() is non empty strict L20()
the carrier of K477() is non zero set
K6( the carrier of K477()) is set
K481() is Element of K6( the carrier of K477())
K7(K481(),K481()) is set
K7(K7(K481(),K481()),COMPLEX) is V33() set
K6(K7(K7(K481(),K481()),COMPLEX)) is set
K489() is Element of K6( the carrier of K477())
K7(K489(),REAL) is V33() V34() V35() set
K6(K7(K489(),REAL)) is set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() set
1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
Prod_real_n is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
0 ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r is complex Element of COMPLEX
0c is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() Element of COMPLEX
- 1r is complex Element of COMPLEX
|.1r.| is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
s is epsilon-transitive epsilon-connected ordinal natural complex 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 * (z #N s) is Element of the carrier of X
s + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 #N s) * z is Element of the carrier of X
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 is non zero 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) . (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 complex 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 * (z #N t) is Element of the carrier of X
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 * (z #N (t + 1)) is Element of the carrier of X
(t + 1) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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) is Element of the carrier of X
z * ((z GeoSeq) . (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
z * (((z GeoSeq) . t) * z) is Element of the carrier of X
(z #N t) * z is Element of the carrier of X
z * ((z #N t) * z) is Element of the carrier of X
(z * (z #N t)) * z is Element of the carrier of X
((z GeoSeq) . (t + 1)) * z is Element of the carrier of X
(z GeoSeq) . ((t + 1) + 1) is Element of the carrier of X
z #N 0 is Element of the carrier of X
z * (z #N 0) is Element of the carrier of X
z * ((z GeoSeq) . 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 complex 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 * (z #N t) is Element of the carrier of X
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 #N t) * z 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 GeoSeq) . (t + 1) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is epsilon-transitive epsilon-connected ordinal natural complex 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
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
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 complex 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
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
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 non zero epsilon-transitive epsilon-connected ordinal natural complex 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
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
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 is non zero 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 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 is non zero 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 * (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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
0. X is zero Element of the carrier of X
z is non zero 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 non zero 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 non zero 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is non zero 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 complex real ext-real Element of REAL
k is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex 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 complex 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 complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is non zero 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 non zero 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 non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
k is complex real ext-real set
p is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
||.z.|| . p is complex real ext-real Element of REAL
z . 1 is Element of the carrier of X
||.(z . 1).|| is complex real ext-real Element of REAL
||.z.|| . 1 is complex 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 complex real ext-real Element of REAL
||.p.|| is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
||.p.|| + k is complex real ext-real Element of REAL
0 + 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
n / (||.p.|| + k) is complex real ext-real Element of REAL
n4 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural complex 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 complex 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 complex real ext-real Element of REAL
z . l is Element of the carrier of X
||.(z . l).|| is complex real ext-real Element of REAL
(z . l) * ((s . l) - p) is Element of the carrier of X
||.((z . l) * ((s . l) - p)).|| is complex real ext-real Element of REAL
||.(z . l).|| * ||.((s . l) - p).|| is complex real ext-real Element of REAL
(z . l) - t is Element of the carrier of X
||.((z . l) - t).|| is complex 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 complex 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 complex 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 complex 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 complex real ext-real Element of REAL
||.(((z . l) - t) * p).|| is complex real ext-real Element of REAL
||.((z . l) * ((s . l) - p)).|| + ||.(((z . l) - t) * p).|| is complex real ext-real Element of REAL
k * (n / (||.p.|| + k)) is complex real ext-real Element of REAL
||.p.|| * ||.((z . l) - t).|| is complex real ext-real Element of REAL
||.p.|| * (n / (||.p.|| + k)) is complex real ext-real Element of REAL
(k * (n / (||.p.|| + k))) + (||.p.|| * (n / (||.p.|| + k))) is complex real ext-real Element of REAL
(n / (||.p.|| + k)) * (||.p.|| + k) is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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 non zero 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 complex 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 complex real ext-real Element of REAL
||.z.|| + 1 is complex real ext-real Element of REAL
0 + 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p / (||.z.|| + 1) is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex 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 complex 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 complex real ext-real Element of REAL
z * ((s . n) - t) is Element of the carrier of X
||.(z * ((s . n) - t)).|| is complex real ext-real Element of REAL
||.z.|| * ||.((s . n) - t).|| is complex real ext-real Element of REAL
||.z.|| * (p / (||.z.|| + 1)) is complex 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 complex real ext-real Element of REAL
0 + ||.z.|| is complex real ext-real Element of REAL
(||.z.|| + 1) * (p / (||.z.|| + 1)) is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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 non zero 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 complex 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 complex real ext-real Element of REAL
||.z.|| + 1 is complex real ext-real Element of REAL
0 + 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p / (||.z.|| + 1) is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex 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 complex 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 complex real ext-real Element of REAL
((s . n) - t) * z is Element of the carrier of X
||.(((s . n) - t) * z).|| is complex real ext-real Element of REAL
||.((s . n) - t).|| * ||.z.|| is complex real ext-real Element of REAL
(p / (||.z.|| + 1)) * ||.z.|| is complex 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 complex real ext-real Element of REAL
0 + ||.z.|| is complex real ext-real Element of REAL
(p / (||.z.|| + 1)) * (||.z.|| + 1) is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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 non zero 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 complex real ext-real Element of REAL
||.z.|| + 1 is complex real ext-real Element of REAL
0 + 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p is complex real ext-real Element of REAL
p / (||.z.|| + 1) is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
||.z.|| * ||.((s . k) - (lim s)).|| is complex real ext-real Element of REAL
||.z.|| * (p / (||.z.|| + 1)) is complex real ext-real Element of REAL
z * ((s . k) - (lim s)) is Element of the carrier of X
||.(z * ((s . k) - (lim s))).|| is complex 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 complex 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 complex real ext-real Element of REAL
0 + ||.z.|| is complex real ext-real Element of REAL
(||.z.|| + 1) * (p / (||.z.|| + 1)) is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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 non zero 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 complex real ext-real Element of REAL
||.z.|| + 1 is complex real ext-real Element of REAL
0 + 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
p is complex real ext-real Element of REAL
p / (||.z.|| + 1) is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
||.((s . k) - (lim s)).|| * ||.z.|| is complex real ext-real Element of REAL
(p / (||.z.|| + 1)) * ||.z.|| is complex real ext-real Element of REAL
((s . k) - (lim s)) * z is Element of the carrier of X
||.(((s . k) - (lim s)) * z).|| is complex 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 complex 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 complex real ext-real Element of REAL
0 + ||.z.|| is complex real ext-real Element of REAL
(p / (||.z.|| + 1)) * (||.z.|| + 1) is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
z is non zero 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 non zero 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 non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
t is complex real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
||.z.|| . n is complex real ext-real Element of REAL
z . 1 is Element of the carrier of X
||.(z . 1).|| is complex real ext-real Element of REAL
||.z.|| . 1 is complex real ext-real Element of REAL
||.(lim s).|| is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
||.(lim s).|| + n is complex real ext-real Element of REAL
0 + 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
k is complex real ext-real Element of REAL
k / (||.(lim s).|| + n) is complex real ext-real Element of REAL
n4 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
||.(lim s).|| * ||.((z . l) - (lim z)).|| is complex real ext-real Element of REAL
||.(lim s).|| * (k / (||.(lim s).|| + n)) is complex 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 complex real ext-real Element of REAL
||.(z . l).|| is complex 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 complex 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 complex 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 complex 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 complex 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 complex real ext-real Element of REAL
||.((z . l) * ((s . l) - (lim s))).|| is complex real ext-real Element of REAL
||.((z . l) * ((s . l) - (lim s))).|| + ||.(((z . l) - (lim z)) * (lim s)).|| is complex real ext-real Element of REAL
||.((s . l) - (lim s)).|| is complex real ext-real Element of REAL
||.(z . l).|| * ||.((s . l) - (lim s)).|| is complex real ext-real Element of REAL
n * (k / (||.(lim s).|| + n)) is complex real ext-real Element of REAL
(n * (k / (||.(lim s).|| + n))) + (||.(lim s).|| * (k / (||.(lim s).|| + n))) is complex real ext-real Element of REAL
(k / (||.(lim s).|| + n)) * (||.(lim s).|| + n) is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 complex 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 non zero epsilon-transitive epsilon-connected ordinal natural complex 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 complex 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 non zero epsilon-transitive epsilon-connected ordinal natural complex 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is non zero 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 non zero 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 complex real ext-real Element of REAL
||.s.|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums ||.s.|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums ||.s.||) . z is complex real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
(Partial_Sums ||.s.||) . t is complex real ext-real Element of REAL
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
||.((Partial_Sums s) . t).|| + ||.(s . (t + 1)).|| is complex real ext-real Element of REAL
((Partial_Sums ||.s.||) . t) + ||.(s . (t + 1)).|| is complex 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 complex real ext-real Element of REAL
(Partial_Sums s) . (t + 1) is Element of the carrier of X
||.((Partial_Sums s) . (t + 1)).|| is complex real ext-real Element of REAL
||.s.|| . (t + 1) is complex real ext-real Element of REAL
((Partial_Sums ||.s.||) . t) + (||.s.|| . (t + 1)) is complex real ext-real Element of REAL
(Partial_Sums ||.s.||) . (t + 1) is complex real ext-real Element of REAL
(Partial_Sums ||.s.||) . 0 is complex real ext-real Element of REAL
||.s.|| . 0 is complex real ext-real Element of REAL
s . 0 is Element of the carrier of X
||.(s . 0).|| is complex real ext-real Element of REAL
(Partial_Sums s) . 0 is Element of the carrier of X
||.((Partial_Sums s) . 0).|| is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is non zero 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 non zero 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 non zero 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 non zero 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 complex 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 non zero epsilon-transitive epsilon-connected ordinal natural complex 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
0. X is zero Element of the carrier of X
z is non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
lim s is complex real ext-real Element of REAL
t is complex real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . p is complex real ext-real Element of REAL
(s . p) - 0 is complex real ext-real Element of REAL
abs ((s . p) - 0) is complex 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 complex real ext-real Element of REAL
||.(z . p).|| is complex real ext-real Element of REAL
abs (s . p) is complex real ext-real Element of REAL
t is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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 non zero 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 complex 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
k ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / (k !) is complex Element of COMPLEX
(1r / (k !)) * (z #N k) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (k !)),(z #N k)) is set
the U11 of X . K23((1r / (k !)),(z #N k)) is set
F₁() is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of F₁() is non zero set
K7(NAT, the carrier of F₁()) is set
K6(K7(NAT, the carrier of F₁())) is set
0. F₁() is zero Element of the carrier of F₁()
X is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
F₂(X,s) is Element of the carrier of F₁()
CHK (s,X) is complex Element of COMPLEX
(CHK (s,X)) * F₂(X,s) is Element of the carrier of F₁()
the U11 of F₁() is Relation-like K7(COMPLEX, the carrier of F₁()) -defined the carrier of F₁() -valued Function-like V26(K7(COMPLEX, the carrier of F₁())) V30(K7(COMPLEX, the carrier of F₁()), the carrier of F₁()) Element of K6(K7(K7(COMPLEX, the carrier of F₁()), the carrier of F₁()))
K7(COMPLEX, the carrier of F₁()) is set
K7(K7(COMPLEX, the carrier of F₁()), the carrier of F₁()) is set
K6(K7(K7(COMPLEX, the carrier of F₁()), the carrier of F₁())) is set
K23((CHK (s,X)),F₂(X,s)) is set
the U11 of F₁() . K23((CHK (s,X)),F₂(X,s)) is set
0c * F₂(X,s) is Element of the carrier of F₁()
K23(0c,F₂(X,s)) is set
the U11 of F₁() . K23(0c,F₂(X,s)) is set
t is set
1r * F₂(X,s) is Element of the carrier of F₁()
K23(1r,F₂(X,s)) is set
the U11 of F₁() . K23(1r,F₂(X,s)) is set
k 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 complex 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 non zero 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 non zero 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 complex 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 complex 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₁()
z is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of z is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of z
Coef X is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
t is Element of the carrier of z
0. z is zero Element of the carrier of z
k is non zero 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 non zero 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 complex 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
(Coef X) . n is complex Element of COMPLEX
((Coef X) . n) * (s #N n) is Element of the carrier of z
the U11 of z is Relation-like K7(COMPLEX, the carrier of z) -defined the carrier of z -valued Function-like V26(K7(COMPLEX, the carrier of z)) V30(K7(COMPLEX, the carrier of z), the carrier of z) Element of K6(K7(K7(COMPLEX, the carrier of z), the carrier of z))
K7(COMPLEX, the carrier of z) is set
K7(K7(COMPLEX, the carrier of z), the carrier of z) is set
K6(K7(K7(COMPLEX, the carrier of z), the carrier of z)) is set
K23(((Coef X) . n),(s #N n)) is set
the U11 of z . K23(((Coef X) . n),(s #N n)) is set
X -' n is epsilon-transitive epsilon-connected ordinal natural complex 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
(((Coef 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 complex 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 complex 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of z is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is Element of the carrier of z
Coef_e X is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
t is Element of the carrier of z
0. z is zero Element of the carrier of z
k is non zero 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 non zero 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 complex 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
(Coef_e X) . n is complex Element of COMPLEX
((Coef_e X) . n) * (s #N n) is Element of the carrier of z
the U11 of z is Relation-like K7(COMPLEX, the carrier of z) -defined the carrier of z -valued Function-like V26(K7(COMPLEX, the carrier of z)) V30(K7(COMPLEX, the carrier of z), the carrier of z) Element of K6(K7(K7(COMPLEX, the carrier of z), the carrier of z))
K7(COMPLEX, the carrier of z) is set
K7(K7(COMPLEX, the carrier of z), the carrier of z) is set
K6(K7(K7(COMPLEX, the carrier of z), the carrier of z)) is set
K23(((Coef_e X) . n),(s #N n)) is set
the U11 of z . K23(((Coef_e X) . n),(s #N n)) is set
X -' n is epsilon-transitive epsilon-connected ordinal natural complex 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
(((Coef_e 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 complex 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 complex 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of z is non zero 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 complex 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 non zero 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 non zero 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 non zero 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 zero Element of the carrier of z
k is non zero 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 non zero 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 complex 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 complex 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 complex 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 complex 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex 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 non zero 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 non zero 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 non zero 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 zero Element of the carrier of X
k is non zero 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 non zero 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 complex 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 complex 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 complex 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 complex 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
1. X is Element of the carrier of X
z is Element of the carrier of X
(X,z) is non zero 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 complex real ext-real Element of REAL
||.z.|| rExpSeq is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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
1r / (s + 1) is complex Element of COMPLEX
(1r / (s + 1)) * z is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (s + 1)),z) is set
the U11 of X . K23((1r / (s + 1)),z) is set
(X,z) . s is Element of the carrier of X
((1r / (s + 1)) * z) * ((X,z) . s) is Element of the carrier of X
||.((X,z) . s).|| is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . s is complex real ext-real Element of REAL
z #N 0 is Element of the carrier of X
1r / (0 !) is complex Element of COMPLEX
(1r / (0 !)) * (z #N 0) is Element of the carrier of X
K23((1r / (0 !)),(z #N 0)) is set
the U11 of X . K23((1r / (0 !)),(z #N 0)) is set
z GeoSeq is non zero 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
(1r / (0 !)) * ((z GeoSeq) . 0) is Element of the carrier of X
K23((1r / (0 !)),((z GeoSeq) . 0)) is set
the U11 of X . K23((1r / (0 !)),((z GeoSeq) . 0)) is set
1r * (1. X) is Element of the carrier of X
K23(1r,(1. X)) is set
the U11 of X . K23(1r,(1. X)) is set
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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
(t + 1) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / ((t + 1) !) is complex Element of COMPLEX
(1r / ((t + 1) !)) * (z #N (t + 1)) is Element of the carrier of X
K23((1r / ((t + 1) !)),(z #N (t + 1))) is set
the U11 of X . K23((1r / ((t + 1) !)),(z #N (t + 1))) is set
(z GeoSeq) . (t + 1) is Element of the carrier of X
(1r / ((t + 1) !)) * ((z GeoSeq) . (t + 1)) is Element of the carrier of X
K23((1r / ((t + 1) !)),((z GeoSeq) . (t + 1))) is set
the U11 of X . K23((1r / ((t + 1) !)),((z GeoSeq) . (t + 1))) is set
(z GeoSeq) . t is Element of the carrier of X
((z GeoSeq) . t) * z is Element of the carrier of X
(1r / ((t + 1) !)) * (((z GeoSeq) . t) * z) is Element of the carrier of X
K23((1r / ((t + 1) !)),(((z GeoSeq) . t) * z)) is set
the U11 of X . K23((1r / ((t + 1) !)),(((z GeoSeq) . t) * z)) is set
z #N t is Element of the carrier of X
(z #N t) * z is Element of the carrier of X
(1r / ((t + 1) !)) * ((z #N t) * z) is Element of the carrier of X
K23((1r / ((t + 1) !)),((z #N t) * z)) is set
the U11 of X . K23((1r / ((t + 1) !)),((z #N t) * z)) is set
t ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(t !) * (t + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
1r / ((t !) * (t + 1)) is complex Element of COMPLEX
(1r / ((t !) * (t + 1))) * ((z #N t) * z) is Element of the carrier of X
K23((1r / ((t !) * (t + 1))),((z #N t) * z)) is set
the U11 of X . K23((1r / ((t !) * (t + 1))),((z #N t) * z)) is set
z * (z #N t) is Element of the carrier of X
1r * 1r is complex Element of COMPLEX
(1r * 1r) / ((t !) * (t + 1)) is complex Element of COMPLEX
((1r * 1r) / ((t !) * (t + 1))) * (z * (z #N t)) is Element of the carrier of X
K23(((1r * 1r) / ((t !) * (t + 1))),(z * (z #N t))) is set
the U11 of X . K23(((1r * 1r) / ((t !) * (t + 1))),(z * (z #N t))) is set
1r / (t !) is complex Element of COMPLEX
1r / (t + 1) is complex Element of COMPLEX
(1r / (t !)) * (1r / (t + 1)) is complex Element of COMPLEX
((1r / (t !)) * (1r / (t + 1))) * (z * (z #N t)) is Element of the carrier of X
K23(((1r / (t !)) * (1r / (t + 1))),(z * (z #N t))) is set
the U11 of X . K23(((1r / (t !)) * (1r / (t + 1))),(z * (z #N t))) is set
(1r / (t + 1)) * z is Element of the carrier of X
K23((1r / (t + 1)),z) is set
the U11 of X . K23((1r / (t + 1)),z) is set
(1r / (t !)) * (z #N t) is Element of the carrier of X
K23((1r / (t !)),(z #N t)) is set
the U11 of X . K23((1r / (t !)),(z #N t)) is set
((1r / (t + 1)) * z) * ((1r / (t !)) * (z #N t)) is Element of the carrier of X
(X,z) . t is Element of the carrier of X
((1r / (t + 1)) * z) * ((X,z) . t) is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
(||.z.|| rExpSeq) . t is complex real ext-real Element of REAL
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
(||.z.|| rExpSeq) . (t + 1) is complex real ext-real Element of REAL
1r / (t + 1) is complex Element of COMPLEX
(1r / (t + 1)) * z is Element of the carrier of X
K23((1r / (t + 1)),z) is set
the U11 of X . K23((1r / (t + 1)),z) is set
||.((1r / (t + 1)) * z).|| is complex real ext-real Element of REAL
(X,z) . t is Element of the carrier of X
||.((X,z) . t).|| is complex real ext-real Element of REAL
||.((1r / (t + 1)) * z).|| * ||.((X,z) . t).|| is complex real ext-real Element of REAL
||.((1r / (t + 1)) * z).|| * ((||.z.|| rExpSeq) . t) is complex real ext-real Element of REAL
((1r / (t + 1)) * z) * ((X,z) . t) is Element of the carrier of X
||.(((1r / (t + 1)) * z) * ((X,z) . t)).|| is complex real ext-real Element of REAL
|.(t + 1).| is complex real ext-real Element of REAL
|.(1r / (t + 1)).| is complex real ext-real Element of REAL
1 / (t + 1) is non zero complex real ext-real positive non negative Element of REAL
(1 / (t + 1)) * ||.z.|| is complex real ext-real Element of REAL
((1 / (t + 1)) * ||.z.||) * ((||.z.|| rExpSeq) . t) is complex real ext-real Element of REAL
((||.z.|| rExpSeq) . t) * ||.z.|| is complex real ext-real Element of REAL
(1 / (t + 1)) * (((||.z.|| rExpSeq) . t) * ||.z.||) is complex real ext-real Element of REAL
||.z.|| |^ t is complex real ext-real Element of REAL
t ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(||.z.|| |^ t) / (t !) is complex real ext-real Element of REAL
((||.z.|| |^ t) / (t !)) * ||.z.|| is complex real ext-real Element of REAL
(1 / (t + 1)) * (((||.z.|| |^ t) / (t !)) * ||.z.||) is complex real ext-real Element of REAL
(||.z.|| |^ t) * ||.z.|| is complex real ext-real Element of REAL
((||.z.|| |^ t) * ||.z.||) / (t !) is complex real ext-real Element of REAL
(1 / (t + 1)) * (((||.z.|| |^ t) * ||.z.||) / (t !)) is complex real ext-real Element of REAL
||.z.|| |^ (t + 1) is complex real ext-real Element of REAL
(||.z.|| |^ (t + 1)) / (t !) is complex real ext-real Element of REAL
(1 / (t + 1)) * ((||.z.|| |^ (t + 1)) / (t !)) is complex real ext-real Element of REAL
(t !) * (t + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(||.z.|| |^ (t + 1)) / ((t !) * (t + 1)) is complex real ext-real Element of REAL
(t + 1) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(||.z.|| |^ (t + 1)) / ((t + 1) !) is complex real ext-real Element of REAL
(X,z) . (t + 1) is Element of the carrier of X
||.((X,z) . (t + 1)).|| is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . 0 is complex real ext-real Element of REAL
||.z.|| |^ 0 is complex real ext-real Element of REAL
(||.z.|| |^ 0) / (0 !) is complex real ext-real Element of REAL
1 / (0 !) is non zero complex real ext-real positive non negative Element of REAL
Prod_real_n . 0 is complex real ext-real Element of REAL
1 / (Prod_real_n . 0) is complex real ext-real Element of REAL
1 / 1 is non zero complex real ext-real positive non negative Element of REAL
(X,z) . 0 is Element of the carrier of X
||.((X,z) . 0).|| is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is non zero 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))
Shift s is non zero 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))
(Shift s) . z is Element of the carrier of X
z -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . (z -' 1) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is non zero 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 non zero 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
Shift s is non zero 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 (Shift s) is non zero 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 (Shift s)) . z is Element of the carrier of X
s . z is Element of the carrier of X
((Partial_Sums (Shift s)) . z) + (s . z) is Element of the carrier of X
t is epsilon-transitive epsilon-connected ordinal natural complex 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 (Shift s)) . t is Element of the carrier of X
s . t is Element of the carrier of X
((Partial_Sums (Shift s)) . t) + (s . t) is Element of the carrier of X
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 (Shift s)) . (t + 1) is Element of the carrier of X
s . (t + 1) is Element of the carrier of X
((Partial_Sums (Shift s)) . (t + 1)) + (s . (t + 1)) is Element of the carrier of X
(((Partial_Sums (Shift s)) . t) + (s . t)) + (s . (t + 1)) is Element of the carrier of X
(Shift s) . (t + 1) is Element of the carrier of X
((Partial_Sums (Shift s)) . t) + ((Shift s) . (t + 1)) is Element of the carrier of X
(((Partial_Sums (Shift s)) . t) + ((Shift 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 zero Element of the carrier of X
(0. X) + (s . 0) is Element of the carrier of X
(Shift s) . 0 is Element of the carrier of X
((Shift s) . 0) + (s . 0) is Element of the carrier of X
(Partial_Sums (Shift s)) . 0 is Element of the carrier of X
((Partial_Sums (Shift s)) . 0) + (s . 0) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is epsilon-transitive epsilon-connected ordinal natural complex 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
(z,X,s,t) is non zero 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 (z,X,s,t) is non zero 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 complex 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
(k,X,s,t) is non zero 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 non zero 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 non zero epsilon-transitive epsilon-connected ordinal natural complex 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
((k + 1),X,s,t) is non zero 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 non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(p + 1) - 1 is complex real ext-real Element of REAL
(k + 1) - 1 is complex real ext-real Element of REAL
k -' p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k -' p) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - p is complex real ext-real Element of REAL
(k - p) + 1 is complex real ext-real Element of REAL
(k + 1) - p is complex real ext-real Element of REAL
(k + 1) -' p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
p ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(k -' p) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(p !) * ((k -' p) !) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(k !) / ((p !) * ((k -' p) !)) is non zero complex real ext-real positive non negative Element of REAL
(k !) * ((k + 1) - p) is complex real ext-real Element of REAL
<i> is complex Element of COMPLEX
0 * <i> is complex set
((k + 1) - p) + (0 * <i>) is complex set
((p !) * ((k -' p) !)) * (((k + 1) - p) + (0 * <i>)) is complex set
((k !) * ((k + 1) - p)) / (((p !) * ((k -' p) !)) * (((k + 1) - p) + (0 * <i>))) is complex Element of COMPLEX
((k -' p) !) * (((k + 1) - p) + (0 * <i>)) is complex set
(p !) * (((k -' p) !) * (((k + 1) - p) + (0 * <i>))) is complex set
((k !) * ((k + 1) - p)) / ((p !) * (((k -' p) !) * (((k + 1) - p) + (0 * <i>)))) is complex Element of COMPLEX
((k + 1) -' p) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(p !) * (((k + 1) -' p) !) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
((k !) * ((k + 1) - p)) / ((p !) * (((k + 1) -' p) !)) is complex real ext-real Element of REAL
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(p -' 1) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p - 1 is complex real ext-real Element of REAL
(p - 1) + 1 is complex real ext-real Element of REAL
k -' (p -' 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - (p -' 1) is complex real ext-real Element of REAL
k - (p - 1) is complex real ext-real Element of REAL
(p -' 1) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(k -' (p -' 1)) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
((p -' 1) !) * ((k -' (p -' 1)) !) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(((p -' 1) !) * ((k -' (p -' 1)) !)) * p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p * ((p -' 1) !) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(p * ((p -' 1) !)) * ((k -' (p -' 1)) !) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p + (0 * <i>) is complex set
(p + (0 * <i>)) * ((p -' 1) !) is complex set
((p + (0 * <i>)) * ((p -' 1) !)) * ((k -' (p -' 1)) !) is complex set
(k !) / (((p -' 1) !) * ((k -' (p -' 1)) !)) is non zero complex real ext-real positive non negative Element of REAL
(k !) * p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((k !) * p) / ((p !) * (((k + 1) -' p) !)) is complex real ext-real non negative Element of REAL
Coef k is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
(Coef k) . p is complex Element of COMPLEX
(Coef k) . (p -' 1) is complex Element of COMPLEX
((Coef k) . p) + ((Coef k) . (p -' 1)) is complex Element of COMPLEX
((k !) / ((p !) * ((k -' p) !))) + ((Coef k) . (p -' 1)) is complex set
((k !) / ((p !) * ((k -' p) !))) + ((k !) / (((p -' 1) !) * ((k -' (p -' 1)) !))) is non zero complex real ext-real positive non negative Element of REAL
((k !) * ((k + 1) - p)) + ((k !) * p) is complex real ext-real Element of REAL
(((k !) * ((k + 1) - p)) + ((k !) * p)) / ((p !) * (((k + 1) -' p) !)) is complex real ext-real Element of REAL
((k + 1) - p) + p is complex real ext-real Element of REAL
(k !) * (((k + 1) - p) + p) is complex real ext-real Element of REAL
((k !) * (((k + 1) - p) + p)) / ((p !) * (((k + 1) -' p) !)) is complex real ext-real Element of REAL
0 + 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
(0 + 0) * <i> is complex set
(((k + 1) - p) + p) + ((0 + 0) * <i>) is complex set
(k !) * ((((k + 1) - p) + p) + ((0 + 0) * <i>)) is complex set
((k !) * ((((k + 1) - p) + p) + ((0 + 0) * <i>))) / ((p !) * (((k + 1) -' p) !)) is complex Element of COMPLEX
(k + 1) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
((k + 1) !) / ((p !) * (((k + 1) -' p) !)) is non zero complex real ext-real positive non negative Element of REAL
Coef (k + 1) is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
(Coef (k + 1)) . p is complex Element of COMPLEX
(k,X,s,t) * t is non zero 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 non zero 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))
Shift ((k,X,s,t) * s) is non zero 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) + (Shift ((k,X,s,t) * s)) is non zero 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) + (Shift ((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
(Shift ((k,X,s,t) * s)) . p is Element of the carrier of X
(((k,X,s,t) * t) . p) + ((Shift ((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) + ((Shift ((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
((Coef k) . p) * (s #N p) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23(((Coef k) . p),(s #N p)) is set
the U11 of X . K23(((Coef k) . p),(s #N p)) is set
t #N (k -' p) is Element of the carrier of X
(((Coef k) . p) * (s #N p)) * (t #N (k -' p)) is Element of the carrier of X
((((Coef k) . p) * (s #N p)) * (t #N (k -' p))) * t is Element of the carrier of X
(((((Coef 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
((Coef k) . (p -' 1)) * (s #N (p -' 1)) is Element of the carrier of X
K23(((Coef k) . (p -' 1)),(s #N (p -' 1))) is set
the U11 of X . K23(((Coef k) . (p -' 1)),(s #N (p -' 1))) is set
t #N (k -' (p -' 1)) is Element of the carrier of X
(((Coef k) . (p -' 1)) * (s #N (p -' 1))) * (t #N (k -' (p -' 1))) is Element of the carrier of X
((((Coef k) . (p -' 1)) * (s #N (p -' 1))) * (t #N (k -' (p -' 1)))) * s is Element of the carrier of X
(((((Coef k) . p) * (s #N p)) * (t #N (k -' p))) * t) + (((((Coef 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
(((Coef k) . p) * (s #N p)) * ((t #N (k -' p)) * t) is Element of the carrier of X
((((Coef k) . p) * (s #N p)) * ((t #N (k -' p)) * t)) + (((((Coef 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
(((Coef k) . p) * (s #N p)) * (t #N ((k -' p) + 1)) is Element of the carrier of X
((((Coef k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + (((((Coef 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
(((Coef k) . (p -' 1)) * (s #N (p -' 1))) * ((t #N (k -' (p -' 1))) * s) is Element of the carrier of X
((((Coef k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + ((((Coef 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
(((Coef k) . (p -' 1)) * (s #N (p -' 1))) * (s * (t #N (k -' (p -' 1)))) is Element of the carrier of X
((((Coef k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + ((((Coef k) . (p -' 1)) * (s #N (p -' 1))) * (s * (t #N (k -' (p -' 1))))) is Element of the carrier of X
(((Coef k) . (p -' 1)) * (s #N (p -' 1))) * s is Element of the carrier of X
((((Coef k) . (p -' 1)) * (s #N (p -' 1))) * s) * (t #N (k -' (p -' 1))) is Element of the carrier of X
((((Coef k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + (((((Coef 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
((Coef k) . (p -' 1)) * ((s #N (p -' 1)) * s) is Element of the carrier of X
K23(((Coef k) . (p -' 1)),((s #N (p -' 1)) * s)) is set
the U11 of X . K23(((Coef k) . (p -' 1)),((s #N (p -' 1)) * s)) is set
(((Coef k) . (p -' 1)) * ((s #N (p -' 1)) * s)) * (t #N (k -' (p -' 1))) is Element of the carrier of X
((((Coef k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + ((((Coef 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
((Coef k) . (p -' 1)) * (s #N ((p -' 1) + 1)) is Element of the carrier of X
K23(((Coef k) . (p -' 1)),(s #N ((p -' 1) + 1))) is set
the U11 of X . K23(((Coef k) . (p -' 1)),(s #N ((p -' 1) + 1))) is set
(((Coef k) . (p -' 1)) * (s #N ((p -' 1) + 1))) * (t #N (k -' (p -' 1))) is Element of the carrier of X
((((Coef k) . p) * (s #N p)) * (t #N ((k -' p) + 1))) + ((((Coef 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
(s #N p) * (t #N ((k + 1) -' p)) is Element of the carrier of X
((Coef k) . p) * ((s #N p) * (t #N ((k + 1) -' p))) is Element of the carrier of X
K23(((Coef k) . p),((s #N p) * (t #N ((k + 1) -' p)))) is set
the U11 of X . K23(((Coef k) . p),((s #N p) * (t #N ((k + 1) -' p)))) is set
((Coef k) . (p -' 1)) * (s #N p) is Element of the carrier of X
K23(((Coef k) . (p -' 1)),(s #N p)) is set
the U11 of X . K23(((Coef k) . (p -' 1)),(s #N p)) is set
(((Coef k) . (p -' 1)) * (s #N p)) * (t #N ((k + 1) -' p)) is Element of the carrier of X
(((Coef k) . p) * ((s #N p) * (t #N ((k + 1) -' p)))) + ((((Coef k) . (p -' 1)) * (s #N p)) * (t #N ((k + 1) -' p))) is Element of the carrier of X
((Coef k) . (p -' 1)) * ((s #N p) * (t #N ((k + 1) -' p))) is Element of the carrier of X
K23(((Coef k) . (p -' 1)),((s #N p) * (t #N ((k + 1) -' p)))) is set
the U11 of X . K23(((Coef k) . (p -' 1)),((s #N p) * (t #N ((k + 1) -' p)))) is set
(((Coef k) . p) * ((s #N p) * (t #N ((k + 1) -' p)))) + (((Coef k) . (p -' 1)) * ((s #N p) * (t #N ((k + 1) -' p)))) is Element of the carrier of X
(((Coef k) . p) + ((Coef k) . (p -' 1))) * ((s #N p) * (t #N ((k + 1) -' p))) is Element of the carrier of X
K23((((Coef k) . p) + ((Coef k) . (p -' 1))),((s #N p) * (t #N ((k + 1) -' p)))) is set
the U11 of X . K23((((Coef k) . p) + ((Coef k) . (p -' 1))),((s #N p) * (t #N ((k + 1) -' p)))) is set
((Coef (k + 1)) . p) * (s #N p) is Element of the carrier of X
K23(((Coef (k + 1)) . p),(s #N p)) is set
the U11 of X . K23(((Coef (k + 1)) . p),(s #N p)) is set
(((Coef (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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k + 1) - 0 is non zero complex real ext-real positive non negative Element of REAL
(Coef (k + 1)) . 0 is complex Element of COMPLEX
1 * ((k + 1) !) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((k + 1) !) / (1 * ((k + 1) !)) is non zero complex real ext-real positive non negative Element of REAL
k -' 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - 0 is complex real ext-real non negative Element of REAL
(Coef k) . 0 is complex Element of COMPLEX
1 * (k !) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k !) / (1 * (k !)) is non zero complex real ext-real positive non negative Element of REAL
((k,X,s,t) * t) . 0 is Element of the carrier of X
(Shift ((k,X,s,t) * s)) . 0 is Element of the carrier of X
(((k,X,s,t) * t) . 0) + ((Shift ((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) + ((Shift ((k,X,s,t) * s)) . 0) is Element of the carrier of X
0. X is zero 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
((Coef k) . 0) * (s #N 0) is Element of the carrier of X
K23(((Coef k) . 0),(s #N 0)) is set
the U11 of X . K23(((Coef k) . 0),(s #N 0)) is set
t #N (k -' 0) is Element of the carrier of X
(((Coef k) . 0) * (s #N 0)) * (t #N (k -' 0)) is Element of the carrier of X
((((Coef 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
(((Coef k) . 0) * (s #N 0)) * ((t #N (k -' 0)) * t) is Element of the carrier of X
((Coef (k + 1)) . 0) * (s #N 0) is Element of the carrier of X
K23(((Coef (k + 1)) . 0),(s #N 0)) is set
the U11 of X . K23(((Coef (k + 1)) . 0),(s #N 0)) is set
t #N ((k + 1) -' 0) is Element of the carrier of X
(((Coef (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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k + 1) - (k + 1) is complex real ext-real Element of REAL
(Coef (k + 1)) . (k + 1) is complex Element of COMPLEX
((k + 1) !) * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((k + 1) !) / (((k + 1) !) * 1) is non zero complex real ext-real positive non negative Element of REAL
k -' k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - k is complex real ext-real Element of REAL
(Coef k) . k is complex Element of COMPLEX
(k !) * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k !) / ((k !) * 1) is non zero complex real ext-real positive non negative Element of REAL
((k,X,s,t) * t) . (k + 1) is Element of the carrier of X
(Shift ((k,X,s,t) * s)) . (k + 1) is Element of the carrier of X
(((k,X,s,t) * t) . (k + 1)) + ((Shift ((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) + ((Shift ((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) + ((Shift ((k,X,s,t) * s)) . (k + 1)) is Element of the carrier of X
(0. X) + ((Shift ((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
((Coef k) . k) * (s #N k) is Element of the carrier of X
K23(((Coef k) . k),(s #N k)) is set
the U11 of X . K23(((Coef k) . k),(s #N k)) is set
t #N (k -' k) is Element of the carrier of X
(((Coef k) . k) * (s #N k)) * (t #N (k -' k)) is Element of the carrier of X
((((Coef 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
(((Coef 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
(((Coef k) . k) * (s #N k)) * (s * (t #N (k -' k))) is Element of the carrier of X
(((Coef k) . k) * (s #N k)) * s is Element of the carrier of X
((((Coef 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
((Coef k) . k) * ((s #N k) * s) is Element of the carrier of X
K23(((Coef k) . k),((s #N k) * s)) is set
the U11 of X . K23(((Coef k) . k),((s #N k) * s)) is set
(((Coef 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
((Coef (k + 1)) . (k + 1)) * (s #N (k + 1)) is Element of the carrier of X
K23(((Coef (k + 1)) . (k + 1)),(s #N (k + 1))) is set
the U11 of X . K23(((Coef (k + 1)) . (k + 1)),(s #N (k + 1))) is set
(((Coef (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 complex 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 non zero 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 non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Partial_Sums (Shift ((k,X,s,t) * s)) is non zero 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 (Shift ((k,X,s,t) * s))) . (k + 1) is Element of the carrier of X
((Partial_Sums (Shift ((k,X,s,t) * s))) . (k + 1)) + (((k,X,s,t) * s) . (k + 1)) is Element of the carrier of X
((Partial_Sums (Shift ((k,X,s,t) * s))) . (k + 1)) + (((k,X,s,t) . (k + 1)) * s) is Element of the carrier of X
((Partial_Sums (Shift ((k,X,s,t) * s))) . (k + 1)) + (0. X) is Element of the carrier of X
(k,X,s,t) * (s + t) is non zero 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 complex 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 non zero 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 is non zero 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
((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)) . k) * (s + t) is Element of the carrier of X
(Partial_Sums (k,X,s,t)) * (s + t) is non zero 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 non zero 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 non zero 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 (Shift ((k,X,s,t) * s))) is non zero 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 (Shift ((k,X,s,t) * s)))) . (k + 1) is Element of the carrier of X
(s + t) #N 0 is Element of the carrier of X
(s + t) GeoSeq is non zero 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) . 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 - 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() Element of REAL
(0,X,s,t) is non zero 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 non zero 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
Coef 0 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
(Coef 0) . 0 is complex Element of COMPLEX
((Coef 0) . 0) * (s #N 0) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23(((Coef 0) . 0),(s #N 0)) is set
the U11 of X . K23(((Coef 0) . 0),(s #N 0)) is set
t #N 0 is Element of the carrier of X
(((Coef 0) . 0) * (s #N 0)) * (t #N 0) is Element of the carrier of X
1r * 1r is complex Element of COMPLEX
1r / (1r * 1r) is complex Element of COMPLEX
(1r / (1r * 1r)) * (s #N 0) is Element of the carrier of X
K23((1r / (1r * 1r)),(s #N 0)) is set
the U11 of X . K23((1r / (1r * 1r)),(s #N 0)) is set
((1r / (1r * 1r)) * (s #N 0)) * (t #N 0) is Element of the carrier of X
(s #N 0) * (t #N 0) is Element of the carrier of X
s GeoSeq is non zero 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
((s GeoSeq) . 0) * (t #N 0) is Element of the carrier of X
t GeoSeq is non zero 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
((s GeoSeq) . 0) * ((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
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(t,X,z,s) is non zero 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 non zero 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 non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / (t !) is complex Element of COMPLEX
(1r / (t !)) * (t,X,z,s) is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
t -' k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(t -' k) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(k !) * ((t -' k) !) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / ((k !) * ((t -' k) !)) is complex Element of COMPLEX
(t !) * 1r is complex set
((t !) * 1r) / (t !) is complex Element of COMPLEX
(((t !) * 1r) / (t !)) / ((k !) * ((t -' k) !)) is complex Element of COMPLEX
(1r / (t !)) * (t !) is complex set
((1r / (t !)) * (t !)) / ((k !) * ((t -' k) !)) is complex Element of COMPLEX
(t,X,z,s) . k is Element of the carrier of X
z #N k is Element of the carrier of X
Coef_e t is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
(Coef_e t) . k is complex Element of COMPLEX
((Coef_e t) . k) * (z #N k) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23(((Coef_e t) . k),(z #N k)) is set
the U11 of X . K23(((Coef_e t) . k),(z #N k)) is set
s #N (t -' k) is Element of the carrier of X
(((Coef_e t) . k) * (z #N k)) * (s #N (t -' k)) is Element of the carrier of X
(1r / ((k !) * ((t -' k) !))) * (z #N k) is Element of the carrier of X
K23((1r / ((k !) * ((t -' k) !))),(z #N k)) is set
the U11 of X . K23((1r / ((k !) * ((t -' k) !))),(z #N k)) is set
((1r / ((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
(((1r / (t !)) * (t !)) / ((k !) * ((t -' k) !))) * ((z #N k) * (s #N (t -' k))) is Element of the carrier of X
K23((((1r / (t !)) * (t !)) / ((k !) * ((t -' k) !))),((z #N k) * (s #N (t -' k)))) is set
the U11 of X . K23((((1r / (t !)) * (t !)) / ((k !) * ((t -' k) !))),((z #N k) * (s #N (t -' k)))) is set
(t !) / ((k !) * ((t -' k) !)) is non zero complex real ext-real positive non negative Element of REAL
(1r / (t !)) * ((t !) / ((k !) * ((t -' k) !))) is complex set
((1r / (t !)) * ((t !) / ((k !) * ((t -' k) !)))) * ((z #N k) * (s #N (t -' k))) is Element of the carrier of X
K23(((1r / (t !)) * ((t !) / ((k !) * ((t -' k) !)))),((z #N k) * (s #N (t -' k)))) is set
the U11 of X . K23(((1r / (t !)) * ((t !) / ((k !) * ((t -' k) !)))),((z #N k) * (s #N (t -' k)))) is set
p is complex Element of COMPLEX
p / ((k !) * ((t -' k) !)) is complex Element of COMPLEX
(p / ((k !) * ((t -' k) !))) * ((z #N k) * (s #N (t -' k))) is Element of the carrier of X
K23((p / ((k !) * ((t -' k) !))),((z #N k) * (s #N (t -' k)))) is set
the U11 of X . K23((p / ((k !) * ((t -' k) !))),((z #N k) * (s #N (t -' k)))) is set
1r / p is complex Element of COMPLEX
(1r / p) * ((p / ((k !) * ((t -' k) !))) * ((z #N k) * (s #N (t -' k)))) is Element of the carrier of X
K23((1r / p),((p / ((k !) * ((t -' k) !))) * ((z #N k) * (s #N (t -' k))))) is set
the U11 of X . K23((1r / p),((p / ((k !) * ((t -' k) !))) * ((z #N k) * (s #N (t -' k))))) is set
(p / ((k !) * ((t -' k) !))) * (z #N k) is Element of the carrier of X
K23((p / ((k !) * ((t -' k) !))),(z #N k)) is set
the U11 of X . K23((p / ((k !) * ((t -' k) !))),(z #N k)) is set
((p / ((k !) * ((t -' k) !))) * (z #N k)) * (s #N (t -' k)) is Element of the carrier of X
(1r / p) * (((p / ((k !) * ((t -' k) !))) * (z #N k)) * (s #N (t -' k))) is Element of the carrier of X
K23((1r / p),(((p / ((k !) * ((t -' k) !))) * (z #N k)) * (s #N (t -' k)))) is set
the U11 of X . K23((1r / p),(((p / ((k !) * ((t -' k) !))) * (z #N k)) * (s #N (t -' k)))) is set
Coef t is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
(Coef t) . k is complex Element of COMPLEX
((Coef t) . k) * (z #N k) is Element of the carrier of X
K23(((Coef t) . k),(z #N k)) is set
the U11 of X . K23(((Coef t) . k),(z #N k)) is set
(((Coef t) . k) * (z #N k)) * (s #N (t -' k)) is Element of the carrier of X
(1r / (t !)) * ((((Coef t) . k) * (z #N k)) * (s #N (t -' k))) is Element of the carrier of X
K23((1r / (t !)),((((Coef t) . k) * (z #N k)) * (s #N (t -' k)))) is set
the U11 of X . K23((1r / (t !)),((((Coef t) . k) * (z #N k)) * (s #N (t -' k)))) is set
(t,X,z,s) . k is Element of the carrier of X
(1r / (t !)) * ((t,X,z,s) . k) is Element of the carrier of X
K23((1r / (t !)),((t,X,z,s) . k)) is set
the U11 of X . K23((1r / (t !)),((t,X,z,s) . k)) is set
((1r / (t !)) * (t,X,z,s)) . k is Element of the carrier of X
0. X is zero Element of the carrier of X
(1r / (t !)) * (0. X) is Element of the carrier of X
K23((1r / (t !)),(0. X)) is set
the U11 of X . K23((1r / (t !)),(0. X)) is set
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
z ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / (z !) is complex Element of COMPLEX
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
(1r / (z !)) * ((s + t) #N z) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (z !)),((s + t) #N z)) is set
the U11 of X . K23((1r / (z !)),((s + t) #N z)) is set
(z,X,s,t) is non zero 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 (z,X,s,t) is non zero 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 non zero 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 non zero 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
(1r / (z !)) * ((Partial_Sums (z,X,s,t)) . z) is Element of the carrier of X
K23((1r / (z !)),((Partial_Sums (z,X,s,t)) . z)) is set
the U11 of X . K23((1r / (z !)),((Partial_Sums (z,X,s,t)) . z)) is set
(1r / (z !)) * (Partial_Sums (z,X,s,t)) is non zero 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))
((1r / (z !)) * (Partial_Sums (z,X,s,t))) . z is Element of the carrier of X
(1r / (z !)) * (z,X,s,t) is non zero 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 ((1r / (z !)) * (z,X,s,t)) is non zero 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 ((1r / (z !)) * (z,X,s,t))) . z is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
0. X is zero Element of the carrier of X
the carrier of X is non zero set
(X,(0. X)) is non zero 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
1. X is Element of the carrier of X
||.(X,(0. X)).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,(0. X)).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
z is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(Partial_Sums ||.(X,(0. X)).||) . z is complex real ext-real Element of REAL
z + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
||.(X,(0. X)).|| . (z + 1) is complex real ext-real Element of REAL
1 + (||.(X,(0. X)).|| . (z + 1)) is complex real ext-real Element of REAL
(X,(0. X)) . (z + 1) is Element of the carrier of X
||.((X,(0. X)) . (z + 1)).|| is complex real ext-real Element of REAL
1 + ||.((X,(0. X)) . (z + 1)).|| is complex real ext-real Element of REAL
1r / (z + 1) is complex Element of COMPLEX
(1r / (z + 1)) * (0. X) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (z + 1)),(0. X)) is set
the U11 of X . K23((1r / (z + 1)),(0. X)) is set
(X,(0. X)) . z is Element of the carrier of X
((1r / (z + 1)) * (0. X)) * ((X,(0. X)) . z) is Element of the carrier of X
||.(((1r / (z + 1)) * (0. X)) * ((X,(0. X)) . z)).|| is complex real ext-real Element of REAL
1 + ||.(((1r / (z + 1)) * (0. X)) * ((X,(0. X)) . z)).|| is complex 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 complex real ext-real Element of REAL
1 + ||.((0. X) * ((X,(0. X)) . z)).|| is complex real ext-real Element of REAL
||.(0. X).|| is complex real ext-real Element of REAL
1 + ||.(0. X).|| is complex real ext-real Element of REAL
1 + 0 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.(X,(0. X)).||) . 0 is complex real ext-real Element of REAL
||.(X,(0. X)).|| . 0 is complex real ext-real Element of REAL
(X,(0. X)) . 0 is Element of the carrier of X
||.((X,(0. X)) . 0).|| is complex real ext-real Element of REAL
||.(1. X).|| is complex real ext-real Element of REAL
Partial_Sums (X,(0. X)) is non zero 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 epsilon-transitive epsilon-connected ordinal natural complex 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 non zero epsilon-transitive epsilon-connected ordinal natural complex 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
1r / (z + 1) is complex Element of COMPLEX
(1r / (z + 1)) * (0. X) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (z + 1)),(0. X)) is set
the U11 of X . K23((1r / (z + 1)),(0. X)) is set
(X,(0. X)) . z is Element of the carrier of X
((1r / (z + 1)) * (0. X)) * ((X,(0. X)) . z) is Element of the carrier of X
(1. X) + (((1r / (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
lim (Partial_Sums (X,(0. X))) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
(X,z) is non zero 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 complex real ext-real Element of REAL
||.z.|| rExpSeq is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
(||.z.|| rExpSeq) . s is complex real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural complex 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
1. X is Element of the carrier of X
z is Element of the carrier of X
(X,z) is non zero 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 non zero 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
1r / (0 !) is complex Element of COMPLEX
(1r / (0 !)) * (z #N 0) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (0 !)),(z #N 0)) is set
the U11 of X . K23((1r / (0 !)),(z #N 0)) is set
z GeoSeq is non zero 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
(1r / (0 !)) * ((z GeoSeq) . 0) is Element of the carrier of X
K23((1r / (0 !)),((z GeoSeq) . 0)) is set
the U11 of X . K23((1r / (0 !)),((z GeoSeq) . 0)) is set
1r * (1. X) is Element of the carrier of X
K23(1r,(1. X)) is set
the U11 of X . K23(1r,(1. X)) is set
0 -' 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Coef 0 is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
(Coef 0) . 0 is complex Element of COMPLEX
((Coef 0) . 0) * (z #N 0) is Element of the carrier of X
K23(((Coef 0) . 0),(z #N 0)) is set
the U11 of X . K23(((Coef 0) . 0),(z #N 0)) is set
s #N 0 is Element of the carrier of X
(((Coef 0) . 0) * (z #N 0)) * (s #N 0) is Element of the carrier of X
1r * 1r is complex Element of COMPLEX
1r / (1r * 1r) is complex Element of COMPLEX
(1r / (1r * 1r)) * (z #N 0) is Element of the carrier of X
K23((1r / (1r * 1r)),(z #N 0)) is set
the U11 of X . K23((1r / (1r * 1r)),(z #N 0)) is set
((1r / (1r * 1r)) * (z #N 0)) * (s #N 0) is Element of the carrier of X
(z #N 0) * (s #N 0) is Element of the carrier of X
((z GeoSeq) . 0) * (s #N 0) is Element of the carrier of X
s GeoSeq is non zero 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
((z GeoSeq) . 0) * ((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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((k + 1),X,z,s) is non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 complex 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
t ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / (t !) is complex Element of COMPLEX
(1r / (t !)) * (z #N t) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (t !)),(z #N t)) is set
the U11 of X . K23((1r / (t !)),(z #N t)) is set
((1r / (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
((k + 1) -' t) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / (((k + 1) -' t) !) is complex Element of COMPLEX
(1r / (((k + 1) -' t) !)) * (s #N ((k + 1) -' t)) is Element of the carrier of X
K23((1r / (((k + 1) -' t) !)),(s #N ((k + 1) -' t))) is set
the U11 of X . K23((1r / (((k + 1) -' t) !)),(s #N ((k + 1) -' t))) is set
((1r / (t !)) * (z #N t)) * ((1r / (((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
(1r / (t !)) * (1r / (((k + 1) -' t) !)) is complex Element of COMPLEX
((1r / (t !)) * (1r / (((k + 1) -' t) !))) * ((z #N t) * (s #N ((k + 1) -' t))) is Element of the carrier of X
K23(((1r / (t !)) * (1r / (((k + 1) -' t) !))),((z #N t) * (s #N ((k + 1) -' t)))) is set
the U11 of X . K23(((1r / (t !)) * (1r / (((k + 1) -' t) !))),((z #N t) * (s #N ((k + 1) -' t)))) is set
1r * 1r is complex Element of COMPLEX
(t !) * (((k + 1) -' t) !) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(1r * 1r) / ((t !) * (((k + 1) -' t) !)) is complex Element of COMPLEX
((1r * 1r) / ((t !) * (((k + 1) -' t) !))) * ((z #N t) * (s #N ((k + 1) -' t))) is Element of the carrier of X
K23(((1r * 1r) / ((t !) * (((k + 1) -' t) !))),((z #N t) * (s #N ((k + 1) -' t)))) is set
the U11 of X . K23(((1r * 1r) / ((t !) * (((k + 1) -' t) !))),((z #N t) * (s #N ((k + 1) -' t)))) is set
Coef_e (k + 1) is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
(Coef_e (k + 1)) . t is complex Element of COMPLEX
((Coef_e (k + 1)) . t) * ((z #N t) * (s #N ((k + 1) -' t))) is Element of the carrier of X
K23(((Coef_e (k + 1)) . t),((z #N t) * (s #N ((k + 1) -' t)))) is set
the U11 of X . K23(((Coef_e (k + 1)) . t),((z #N t) * (s #N ((k + 1) -' t)))) is set
((Coef_e (k + 1)) . t) * (z #N t) is Element of the carrier of X
K23(((Coef_e (k + 1)) . t),(z #N t)) is set
the U11 of X . K23(((Coef_e (k + 1)) . t),(z #N t)) is set
(((Coef_e (k + 1)) . t) * (z #N t)) * (s #N ((k + 1) -' t)) is Element of the carrier of X
(k + 1) - t is complex real ext-real Element of REAL
k - t is complex real ext-real Element of REAL
(k - t) + 1 is complex real ext-real Element of REAL
k -' t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(k -' t) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Partial_Sums (X,s) is non zero 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((t + 1),X,z,s) is non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 complex 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 non zero 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 non zero 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 non zero 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
(X,z) is non zero 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 complex 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 non zero 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 complex real ext-real Element of REAL
t -' t is epsilon-transitive epsilon-connected ordinal natural complex 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
Coef_e t is non zero Relation-like NAT -defined COMPLEX -valued Function-like V26( NAT ) V30( NAT , COMPLEX ) V33() Element of K6(K7(NAT,COMPLEX))
(Coef_e t) . t is complex Element of COMPLEX
((Coef_e t) . t) * (z #N t) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23(((Coef_e t) . t),(z #N t)) is set
the U11 of X . K23(((Coef_e t) . t),(z #N t)) is set
s #N 0 is Element of the carrier of X
(((Coef_e t) . t) * (z #N t)) * (s #N 0) is Element of the carrier of X
1. X is Element of the carrier of X
(((Coef_e t) . t) * (z #N t)) * (1. X) is Element of the carrier of X
t ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(t !) * 1r is complex set
1r / ((t !) * 1r) is complex Element of COMPLEX
(1r / ((t !) * 1r)) * (z #N t) is Element of the carrier of X
K23((1r / ((t !) * 1r)),(z #N t)) is set
the U11 of X . K23((1r / ((t !) * 1r)),(z #N t)) is set
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is epsilon-transitive epsilon-connected ordinal natural complex 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 non zero 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 non zero 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 non zero 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 non zero 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 complex 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 non zero 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 non zero 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 non zero epsilon-transitive epsilon-connected ordinal natural complex 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 non zero 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 non zero 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 complex 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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
(k + 1) ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / ((k + 1) !) is complex Element of COMPLEX
(1r / ((k + 1) !)) * ((s + t) #N (k + 1)) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / ((k + 1) !)),((s + t) #N (k + 1))) is set
the U11 of X . K23((1r / ((k + 1) !)),((s + t) #N (k + 1))) is set
(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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(0,X,s,t) is non zero 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 non zero 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 non zero 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 non zero 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 non zero 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is epsilon-transitive epsilon-connected ordinal natural complex 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 non zero 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 complex 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 complex 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
||.z.|| is complex real ext-real Element of REAL
||.z.|| rExpSeq is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(||.z.|| rExpSeq) . s is complex real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.z.|| |^ t is complex real ext-real Element of REAL
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.z.|| |^ (t + 1) is complex real ext-real Element of REAL
(||.z.|| |^ t) * ||.z.|| is complex real ext-real Element of REAL
||.z.|| |^ 0 is complex real ext-real Element of REAL
||.z.|| |^ s is complex real ext-real Element of REAL
s ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(||.z.|| |^ s) / (s !) is complex real ext-real Element of REAL
(s !) " is non zero complex real ext-real positive non negative Element of REAL
(||.z.|| |^ s) * ((s !) ") is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
(X,z) is non zero 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 non zero 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 complex real ext-real Element of REAL
||.z.|| rExpSeq is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (||.z.|| rExpSeq) is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Sum (||.z.|| rExpSeq) is complex real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . s is complex real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . 0 is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . 0 is complex real ext-real Element of REAL
||.z.|| |^ 0 is complex real ext-real Element of REAL
(||.z.|| |^ 0) / (0 !) is complex real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . t is complex real ext-real Element of REAL
t + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . (t + 1) is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . (t + 1) is complex real ext-real Element of REAL
||.((Partial_Sums (X,z)) . t).|| + ((||.z.|| rExpSeq) . (t + 1)) is complex real ext-real Element of REAL
((Partial_Sums (||.z.|| rExpSeq)) . t) + ((||.z.|| rExpSeq) . (t + 1)) is complex 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 complex real ext-real Element of REAL
||.((X,z) . (t + 1)).|| is complex real ext-real Element of REAL
||.((Partial_Sums (X,z)) . t).|| + ||.((X,z) . (t + 1)).|| is complex real ext-real Element of REAL
(Partial_Sums (X,z)) . 0 is Element of the carrier of X
||.((Partial_Sums (X,z)) . 0).|| is complex real ext-real Element of REAL
(X,z) . 0 is Element of the carrier of X
||.((X,z) . 0).|| is complex real ext-real Element of REAL
z #N 0 is Element of the carrier of X
1r / (0 !) is complex Element of COMPLEX
(1r / (0 !)) * (z #N 0) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (0 !)),(z #N 0)) is set
the U11 of X . K23((1r / (0 !)),(z #N 0)) is set
||.((1r / (0 !)) * (z #N 0)).|| is complex real ext-real Element of REAL
z GeoSeq is non zero 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
(1r / (0 !)) * ((z GeoSeq) . 0) is Element of the carrier of X
K23((1r / (0 !)),((z GeoSeq) . 0)) is set
the U11 of X . K23((1r / (0 !)),((z GeoSeq) . 0)) is set
||.((1r / (0 !)) * ((z GeoSeq) . 0)).|| is complex real ext-real Element of REAL
1. X is Element of the carrier of X
1r * (1. X) is Element of the carrier of X
K23(1r,(1. X)) is set
the U11 of X . K23(1r,(1. X)) is set
||.(1r * (1. X)).|| is complex real ext-real Element of REAL
||.(1. X).|| is complex real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(||.z.|| rExpSeq) . t is complex real ext-real Element of REAL
lim (Partial_Sums (||.z.|| rExpSeq)) is complex real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (||.z.|| rExpSeq)) . t is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
||.z.|| is complex real ext-real Element of REAL
||.z.|| rExpSeq is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Sum (||.z.|| rExpSeq) is complex real ext-real Element of REAL
(X,z) is non zero 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 non zero 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 complex real ext-real Element of REAL
(X,z) . 0 is Element of the carrier of X
||.((X,z) . 0).|| is complex real ext-real Element of REAL
1. X is Element of the carrier of X
||.(1. X).|| is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
||.z.|| is complex real ext-real Element of REAL
||.z.|| rExpSeq is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (||.z.|| rExpSeq) is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (||.z.|| rExpSeq)) . s is complex real ext-real Element of REAL
abs ((Partial_Sums (||.z.|| rExpSeq)) . s) is complex real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (||.z.|| rExpSeq)) . t is complex real ext-real Element of REAL
((Partial_Sums (||.z.|| rExpSeq)) . t) - ((Partial_Sums (||.z.|| rExpSeq)) . s) is complex real ext-real Element of REAL
abs (((Partial_Sums (||.z.|| rExpSeq)) . t) - ((Partial_Sums (||.z.|| rExpSeq)) . s)) is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(||.z.|| rExpSeq) . k is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z,s,t) is non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,t).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.(X,z,s,t).||) . k is complex real ext-real Element of REAL
abs ((Partial_Sums ||.(X,z,s,t).||) . k) is complex real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X,z,s,t).|| . p is complex real ext-real Element of REAL
(X,z,s,t) . p is Element of the carrier of X
||.((X,z,s,t) . p).|| is complex real ext-real Element of REAL
(Partial_Sums ||.(X,z,s,t).||) . 0 is complex real ext-real Element of REAL
||.(X,z,s,t).|| . 0 is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
s is Element of the carrier of X
t is complex real ext-real set
k is complex real ext-real Element of REAL
4 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.z.|| is complex real ext-real Element of REAL
||.z.|| rExpSeq is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Sum (||.z.|| rExpSeq) is complex real ext-real Element of REAL
4 * (Sum (||.z.|| rExpSeq)) is complex real ext-real Element of REAL
k / (4 * (Sum (||.z.|| rExpSeq))) is complex real ext-real Element of REAL
||.s.|| is complex real ext-real Element of REAL
||.s.|| rExpSeq is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Sum (||.s.|| rExpSeq) is complex real ext-real Element of REAL
4 * (Sum (||.s.|| rExpSeq)) is complex real ext-real Element of REAL
k / (4 * (Sum (||.s.|| rExpSeq))) is complex real ext-real Element of REAL
min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq))))) is complex real ext-real Element of REAL
(X,s) is non zero 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 non zero 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 complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Partial_Sums (||.z.|| rExpSeq) is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural complex 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 complex 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n4 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z) is non zero 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 complex 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 complex real ext-real Element of REAL
||.((X,z) . l).|| is complex real ext-real Element of REAL
||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is complex real ext-real Element of REAL
||.((X,z) . l).|| * ||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . l is complex real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is complex real ext-real Element of REAL
(X,z,s,l) is non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
||.(X,z,s,l).|| . l is complex real ext-real Element of REAL
(X,z,s,l) . l is Element of the carrier of X
||.((X,z,s,l) . l).|| is complex real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X,z,s,l).|| . l is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . l is complex real ext-real Element of REAL
l -' l is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (X,s)) . l) - ((Partial_Sums (X,s)) . (l -' l))).|| is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex 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 complex 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 complex 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 complex real ext-real Element of REAL
||.((Partial_Sums (X,s)) . k).|| is complex real ext-real Element of REAL
||.((Partial_Sums (X,s)) . (k -' l)).|| is complex real ext-real Element of REAL
||.((Partial_Sums (X,s)) . k).|| + ||.((Partial_Sums (X,s)) . (k -' l)).|| is complex real ext-real Element of REAL
(Sum (||.s.|| rExpSeq)) + ||.((Partial_Sums (X,s)) . (k -' l)).|| is complex real ext-real Element of REAL
(Sum (||.s.|| rExpSeq)) + (Sum (||.s.|| rExpSeq)) is complex real ext-real Element of REAL
2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
2 * (Sum (||.s.|| rExpSeq)) is complex real ext-real Element of REAL
(X,z,s,k) is non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
||.(X,z,s,k).|| . l is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . l is complex real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (X,s)) . k) - ((Partial_Sums (X,s)) . (k -' l))).|| is complex real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * (2 * (Sum (||.s.|| rExpSeq))) is complex real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X,z,s,k).|| . l is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . l is complex real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * (2 * (Sum (||.s.|| rExpSeq))) is complex real ext-real Element of REAL
t / (4 * (Sum (||.s.|| rExpSeq))) is complex real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * (t / (4 * (Sum (||.s.|| rExpSeq)))) is complex real ext-real Element of REAL
(4 * (Sum (||.s.|| rExpSeq))) " is complex real ext-real Element of REAL
t * ((4 * (Sum (||.s.|| rExpSeq))) ") is complex real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * (t * ((4 * (Sum (||.s.|| rExpSeq))) ")) is complex real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * t is complex real ext-real Element of REAL
((2 * (Sum (||.s.|| rExpSeq))) * t) * ((4 * (Sum (||.s.|| rExpSeq))) ") is complex real ext-real Element of REAL
2 * t is complex real ext-real Element of REAL
(2 * t) * (Sum (||.s.|| rExpSeq)) is complex real ext-real Element of REAL
((2 * t) * (Sum (||.s.|| rExpSeq))) / (4 * (Sum (||.s.|| rExpSeq))) is complex real ext-real Element of REAL
(2 * t) / 4 is complex real ext-real Element of REAL
t / 2 is complex real ext-real Element of REAL
t / (4 * (Sum (||.z.|| rExpSeq))) is complex real ext-real Element of REAL
(Sum (||.z.|| rExpSeq)) * (t / (4 * (Sum (||.z.|| rExpSeq)))) is complex real ext-real Element of REAL
(4 * (Sum (||.z.|| rExpSeq))) " is complex real ext-real Element of REAL
t * ((4 * (Sum (||.z.|| rExpSeq))) ") is complex real ext-real Element of REAL
(Sum (||.z.|| rExpSeq)) * (t * ((4 * (Sum (||.z.|| rExpSeq))) ")) is complex real ext-real Element of REAL
(Sum (||.z.|| rExpSeq)) * t is complex real ext-real Element of REAL
((Sum (||.z.|| rExpSeq)) * t) * ((4 * (Sum (||.z.|| rExpSeq))) ") is complex real ext-real Element of REAL
((Sum (||.z.|| rExpSeq)) * t) / (4 * (Sum (||.z.|| rExpSeq))) is complex real ext-real Element of REAL
t / 4 is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex 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 complex 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 complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k - (n + n) is complex real ext-real Element of REAL
(k -' (n + n)) + (n + n) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((n + n) + (n + n)) - (n + n) is complex real ext-real Element of REAL
((n + n) + (n + n)) - l is complex real ext-real Element of REAL
n4 - l is complex real ext-real Element of REAL
k - l is complex real ext-real Element of REAL
0 + n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z,s,k) is non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
||.(X,z,s,k).|| . l is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . l is complex 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 complex 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 complex real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (X,s)) . k) - ((Partial_Sums (X,s)) . (k -' l))).|| is complex real ext-real Element of REAL
((||.z.|| rExpSeq) . l) * (min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) is complex real ext-real Element of REAL
(min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) is complex real ext-real Element of REAL
Partial_Sums ||.(X,z,s,k).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,k).||) . (n + n) is complex real ext-real Element of REAL
(Partial_Sums (||.z.|| rExpSeq)) . (n + n) is complex real ext-real Element of REAL
((Partial_Sums (||.z.|| rExpSeq)) . (n + n)) * (min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) is complex real ext-real Element of REAL
n + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (||.z.|| rExpSeq)) . k is complex real ext-real Element of REAL
((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n + n)) is complex real ext-real Element of REAL
abs (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n + n))) is complex real ext-real Element of REAL
(((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n + n))) * (2 * (Sum (||.s.|| rExpSeq))) is complex real ext-real Element of REAL
(min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) * (2 * (Sum (||.s.|| rExpSeq))) is complex real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X,z,s,k).|| . l is complex real ext-real Element of REAL
(||.z.|| rExpSeq) . l is complex real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * ((||.z.|| rExpSeq) . l) is complex real ext-real Element of REAL
(Partial_Sums ||.(X,z,s,k).||) . k is complex real ext-real Element of REAL
((Partial_Sums ||.(X,z,s,k).||) . k) - ((Partial_Sums ||.(X,z,s,k).||) . (n + n)) is complex real ext-real Element of REAL
(t / 4) + (t / 4) is complex real ext-real Element of REAL
0 + (t / 4) is complex real ext-real Element of REAL
(Sum (||.z.|| rExpSeq)) * (min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) is complex real ext-real Element of REAL
(2 * (Sum (||.s.|| rExpSeq))) * (min ((k / (4 * (Sum (||.z.|| rExpSeq)))),(k / (4 * (Sum (||.s.|| rExpSeq)))))) is complex real ext-real Element of REAL
(t / 2) + (t / 2) is complex 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 complex real ext-real Element of REAL
abs ((Partial_Sums ||.(X,z,s,k).||) . k) is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,z,s,k) is non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,k).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,k).||) . k is complex real ext-real Element of REAL
abs ((Partial_Sums ||.(X,z,s,k).||) . k) is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
0. X is zero Element of the carrier of X
z is Element of the carrier of X
s is Element of the carrier of X
t is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
t is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
k is non zero 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 complex 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 complex real ext-real Element of REAL
(X,z,s,p) is non zero 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 non zero 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 complex real ext-real Element of REAL
||.(X,z,s,p).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,p).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,p).||) . p is complex real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural complex 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 complex real ext-real Element of REAL
(X,z,s,p) is non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,p).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,p).||) . p is complex real ext-real Element of REAL
t . p is complex real ext-real Element of REAL
p is complex real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t . k is complex real ext-real Element of REAL
(t . k) - 0 is complex real ext-real Element of REAL
abs ((t . k) - 0) is complex real ext-real Element of REAL
(X,z,s,k) is non zero 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 non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums ||.(X,z,s,k).|| is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums ||.(X,z,s,k).||) . k is complex real ext-real Element of REAL
abs ((Partial_Sums ||.(X,z,s,k).||) . k) is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
t . k is complex real ext-real Element of REAL
(t . k) - 0 is complex real ext-real Element of REAL
abs ((t . k) - 0) is complex real ext-real Element of REAL
lim t is complex real ext-real Element of REAL
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
(X,z) is non zero 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
s is Element of the carrier of X
(X,s) is non zero 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
(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 non zero 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
t is non zero 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 non zero 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 complex 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 non zero 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 non zero 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) is non zero 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)) . k is Element of the carrier of X
Partial_Sums (X,s) is non zero 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 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)) is non zero 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 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 non zero 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 non zero 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 zero 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)) is Element of the carrier of X
lim (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
lim (Partial_Sums (X,(z + s))) is Element of the carrier of X
(Sum (X,z)) * (lim (Partial_Sums (X,s))) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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 non zero 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 non zero 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 non zero 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
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
(X) is non zero 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
(X,z) is Element of the carrier of X
(X) is non zero 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 non zero 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
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
(X,z) is Element of the carrier of X
(X) is non zero 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 non zero 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
(X,s) is non zero 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
(X,z) is non zero 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
(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 non zero 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
(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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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 non zero 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 non zero 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 complex 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
t ! is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / (t !) is complex Element of COMPLEX
(1r / (t !)) * (s #N t) is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((1r / (t !)),(s #N t)) is set
the U11 of X . K23((1r / (t !)),(s #N t)) is set
z * ((1r / (t !)) * (s #N t)) is Element of the carrier of X
z * (s #N t) is Element of the carrier of X
(1r / (t !)) * (z * (s #N t)) is Element of the carrier of X
K23((1r / (t !)),(z * (s #N t))) is set
the U11 of X . K23((1r / (t !)),(z * (s #N t))) is set
(s #N t) * z is Element of the carrier of X
(1r / (t !)) * ((s #N t) * z) is Element of the carrier of X
K23((1r / (t !)),((s #N t) * z)) is set
the U11 of X . K23((1r / (t !)),((s #N t) * z)) is set
((1r / (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 non zero 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 non zero 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
z * (Sum (X,s)) is Element of the carrier of X
lim (Partial_Sums (X,s)) is Element of the carrier of X
z * (lim (Partial_Sums (X,s))) is Element of the carrier of X
z * (Partial_Sums (X,s)) is non zero 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 non zero 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 non zero 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
(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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
0. X is zero Element of the carrier of X
the carrier of X is non zero set
(X,(0. X)) is Element of the carrier of X
(X) is non zero 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 non zero 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
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero 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 non zero 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
(- 1r) * z is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23((- 1r),z) is set
the U11 of X . K23((- 1r),z) is set
z * ((- 1r) * z) is Element of the carrier of X
z * z is Element of the carrier of X
(- 1r) * (z * z) is Element of the carrier of X
K23((- 1r),(z * z)) is set
the U11 of X . K23((- 1r),(z * z)) is set
((- 1r) * 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 zero 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
(X,z) is Element of the carrier of X
(X) is non zero 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() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
s is complex set
s * z is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23(s,z) is set
the U11 of X . K23(s,z) is set
t is complex set
t * z is Element of the carrier of X
K23(t,z) is set
the U11 of X . K23(t,z) is set
(s * z) * (t * z) is Element of the carrier of X
z * z is Element of the carrier of X
s * t is complex set
(s * t) * (z * z) is Element of the carrier of X
K23((s * t),(z * z)) is set
the U11 of X . K23((s * t),(z * z)) is set
(t * z) * (s * z) is Element of the carrier of X
X is non empty right_complementable V126() V127() V128() V136() V137() V155() V159() V160() V161() V162() V164() V181() V182() V183() V184() V187() V194() V196() V198() V199() V200() V201() Normed_Complex_AlgebraStr
the carrier of X is non zero set
z is Element of the carrier of X
s is complex set
s * z is Element of the carrier of X
the U11 of X is Relation-like K7(COMPLEX, the carrier of X) -defined the carrier of X -valued Function-like V26(K7(COMPLEX, the carrier of X)) V30(K7(COMPLEX, the carrier of X), the carrier of X) Element of K6(K7(K7(COMPLEX, the carrier of X), the carrier of X))
K7(COMPLEX, the carrier of X) is set
K7(K7(COMPLEX, the carrier of X), the carrier of X) is set
K6(K7(K7(COMPLEX, the carrier of X), the carrier of X)) is set
K23(s,z) is set
the U11 of X . K23(s,z) is set
(X,(s * z)) is Element of the carrier of X
(X) is non zero 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 complex set
t * z is Element of the carrier of X
K23(t,z) is set
the U11 of X . K23(t,z) is set
(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 complex set
(s + t) * z is Element of the carrier of X
K23((s + t),z) is set
the U11 of X . K23((s + t),z) is set
(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 complex set
(t + s) * z is Element of the carrier of X
K23((t + s),z) is set
the U11 of X . K23((t + s),z) is set
(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