:: 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

the carrier of F

K7(NAT, the carrier of F

K6(K7(NAT, the carrier of F

0. 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

CHK (s,X) is complex Element of COMPLEX

(CHK (s,X)) * F

the U11 of F

K7(COMPLEX, the carrier of F

K7(K7(COMPLEX, the carrier of F

K6(K7(K7(COMPLEX, the carrier of F

K23((CHK (s,X)),F

the U11 of F

0c * F

K23(0c,F

the U11 of F

t is set

1r * F

K23(1r,F

the U11 of F

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

s is non zero Relation-like NAT -defined the carrier of F

t is non zero Relation-like NAT -defined 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

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

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