:: LOPBAN_4 semantic presentation

REAL is V1() V47() V59() V60() V61() V65() set

NAT is V1() epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() Element of K6(REAL)

K6(REAL) is set

COMPLEX is V1() V47() V59() V65() set

omega is V1() epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() set

K6(omega) is set

K6(NAT) is set

RAT is V1() V47() V59() V60() V61() V62() V65() set

INT is V1() V47() V59() V60() V61() V62() V63() V65() set

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

K6(K7(NAT,REAL)) is set

K7(NAT,COMPLEX) is complex-valued set

K6(K7(NAT,COMPLEX)) is set

K7(COMPLEX,COMPLEX) is complex-valued set

K6(K7(COMPLEX,COMPLEX)) is set

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

K6(K7(REAL,REAL)) is set

K380() is V1() set

K7(K380(),K380()) is set

K7(K7(K380(),K380()),K380()) is set

K6(K7(K7(K380(),K380()),K380())) is set

K7(REAL,K380()) is set

K7(K7(REAL,K380()),K380()) is set

K6(K7(K7(REAL,K380()),K380())) is set

K386() is L12()

the carrier of K386() is set

K6( the carrier of K386()) is set

K390() is Element of K6( the carrier of K386())

K7(K390(),K390()) is set

K7(K7(K390(),K390()),REAL) is complex-valued ext-real-valued real-valued set

K6(K7(K7(K390(),K390()),REAL)) is set

the_set_of_l1RealSequences is Element of K6( the carrier of K386())

K7(the_set_of_l1RealSequences,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(the_set_of_l1RealSequences,REAL)) is set

0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() set

1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

Prod_real_n is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

0 ! is V11() real ext-real Element of REAL

- 1 is V11() real ext-real non positive Element of REAL

4 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X is non empty multMagma

the carrier of X is V1() set

t is Element of the carrier of X

t * t is Element of the carrier of X

t is Element of the carrier of X

k is Element of the carrier of X

t * k is Element of the carrier of X

k * t is Element of the carrier of X

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

z is Element of the carrier of X

s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z #N s is Element of the carrier of X

z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

(z GeoSeq) . s is Element of the carrier of X

z * (z #N s) is Element of the carrier of X

s + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z #N (s + 1) is Element of the carrier of X

(z GeoSeq) . (s + 1) is Element of the carrier of X

(z #N s) * z is Element of the carrier of X

0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z #N (0 + 1) is Element of the carrier of X

(z GeoSeq) . (0 + 1) is Element of the carrier of X

(z GeoSeq) . 0 is Element of the carrier of X

((z GeoSeq) . 0) * z is Element of the carrier of X

1. X is Element of the carrier of X

(1. X) * z is Element of the carrier of X

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z #N t is Element of the carrier of X

(z GeoSeq) . t is Element of the carrier of X

z * (z #N t) is Element of the carrier of X

t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z #N (t + 1) is Element of the carrier of X

(z GeoSeq) . (t + 1) is Element of the carrier of X

z * (z #N (t + 1)) is Element of the carrier of X

(t + 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z #N ((t + 1) + 1) is Element of the carrier of X

(z GeoSeq) . ((t + 1) + 1) is Element of the carrier of X

(z GeoSeq) . t is Element of the carrier of X

((z GeoSeq) . t) * z is Element of the carrier of X

z * (((z GeoSeq) . t) * z) is Element of the carrier of X

(z * (z #N t)) * z is Element of the carrier of X

z #N 0 is Element of the carrier of X

(z GeoSeq) . 0 is Element of the carrier of X

z * (z #N 0) is Element of the carrier of X

z * (1. X) is Element of the carrier of X

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z #N t is Element of the carrier of X

(z GeoSeq) . t is Element of the carrier of X

z * (z #N t) is Element of the carrier of X

t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z #N (t + 1) is Element of the carrier of X

(z GeoSeq) . (t + 1) is Element of the carrier of X

(z #N t) * z is Element of the carrier of X

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s is Element of the carrier of X

s #N z is Element of the carrier of X

s GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

(s GeoSeq) . z is Element of the carrier of X

t is Element of the carrier of X

t * (s #N z) is Element of the carrier of X

(s #N z) * t is Element of the carrier of X

t #N z is Element of the carrier of X

t GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

(t GeoSeq) . z is Element of the carrier of X

s * (t #N z) is Element of the carrier of X

(t #N z) * s is Element of the carrier of X

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s #N k is Element of the carrier of X

(s GeoSeq) . k is Element of the carrier of X

t * (s #N k) is Element of the carrier of X

(s #N k) * t is Element of the carrier of X

t #N k is Element of the carrier of X

(t GeoSeq) . k is Element of the carrier of X

s * (t #N k) is Element of the carrier of X

(t #N k) * s is Element of the carrier of X

k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s #N (k + 1) is Element of the carrier of X

(s GeoSeq) . (k + 1) is Element of the carrier of X

t * (s #N (k + 1)) is Element of the carrier of X

(s #N (k + 1)) * t is Element of the carrier of X

t #N (k + 1) is Element of the carrier of X

(t GeoSeq) . (k + 1) is Element of the carrier of X

s * (t #N (k + 1)) is Element of the carrier of X

(t #N (k + 1)) * s is Element of the carrier of X

(t #N k) * t is Element of the carrier of X

s * ((t #N k) * t) is Element of the carrier of X

(s * (t #N k)) * t is Element of the carrier of X

s * t is Element of the carrier of X

(t #N k) * (s * t) is Element of the carrier of X

t * s is Element of the carrier of X

(t #N k) * (t * s) is Element of the carrier of X

((t #N k) * t) * s is Element of the carrier of X

(s #N k) * s is Element of the carrier of X

t * ((s #N k) * s) is Element of the carrier of X

(t * (s #N k)) * s is Element of the carrier of X

(s #N k) * (t * s) is Element of the carrier of X

(s #N k) * (s * t) is Element of the carrier of X

((s #N k) * s) * t is Element of the carrier of X

t #N 0 is Element of the carrier of X

(t GeoSeq) . 0 is Element of the carrier of X

1. X is Element of the carrier of X

s * (t #N 0) is Element of the carrier of X

(t #N 0) * s is Element of the carrier of X

s #N 0 is Element of the carrier of X

(s GeoSeq) . 0 is Element of the carrier of X

t * (s #N 0) is Element of the carrier of X

(s #N 0) * t is Element of the carrier of X

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

0. X is V82(X) Element of the carrier of X

z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim z is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

z - s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim (z - s) is Element of the carrier of X

lim s is Element of the carrier of X

(lim z) - (lim s) is Element of the carrier of X

((lim z) - (lim s)) + (lim s) is Element of the carrier of X

(lim s) - (lim s) is Element of the carrier of X

(lim z) - ((lim s) - (lim s)) is Element of the carrier of X

(lim z) - (0. X) is Element of the carrier of X

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim z is Element of the carrier of X

s is Element of the carrier of X

t is V11() real ext-real Element of REAL

k is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z . p is Element of the carrier of X

(z . p) - s is Element of the carrier of X

||.((z . p) - s).|| is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

t is Element of the carrier of X

||.z.|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

k is V11() real ext-real set

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z . p is Element of the carrier of X

||.(z . p).|| is V11() real ext-real Element of REAL

||.z.|| . p is V11() real ext-real Element of REAL

z . 1 is Element of the carrier of X

||.(z . 1).|| is V11() real ext-real Element of REAL

||.z.|| . 1 is V11() real ext-real Element of REAL

p is Element of the carrier of X

t * p is Element of the carrier of X

n is Element of the carrier of X

n is V11() real ext-real Element of REAL

||.p.|| is V11() real ext-real Element of REAL

k is V11() real ext-real Element of REAL

||.p.|| + k is V11() real ext-real Element of REAL

0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

n / (||.p.|| + k) is V11() real ext-real Element of REAL

n4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

n4 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(z * s) . l is Element of the carrier of X

((z * s) . l) - n is Element of the carrier of X

||.(((z * s) . l) - n).|| is V11() real ext-real Element of REAL

s . l is Element of the carrier of X

(s . l) - p is Element of the carrier of X

||.((s . l) - p).|| is V11() real ext-real Element of REAL

z . l is Element of the carrier of X

||.(z . l).|| is V11() real ext-real Element of REAL

(z . l) * ((s . l) - p) is Element of the carrier of X

||.((z . l) * ((s . l) - p)).|| is V11() real ext-real Element of REAL

||.(z . l).|| * ||.((s . l) - p).|| is V11() real ext-real Element of REAL

(z . l) - t is Element of the carrier of X

||.((z . l) - t).|| is V11() real ext-real Element of REAL

(z * s) . l is Element of the carrier of X

((z * s) . l) - n is Element of the carrier of X

||.(((z * s) . l) - n).|| is V11() real ext-real Element of REAL

(z . l) * (s . l) is Element of the carrier of X

((z . l) * (s . l)) - (t * p) is Element of the carrier of X

||.(((z . l) * (s . l)) - (t * p)).|| is V11() real ext-real Element of REAL

(z . l) * p is Element of the carrier of X

((z . l) * (s . l)) - ((z . l) * p) is Element of the carrier of X

((z . l) * p) - (t * p) is Element of the carrier of X

(((z . l) * (s . l)) - ((z . l) * p)) + (((z . l) * p) - (t * p)) is Element of the carrier of X

||.((((z . l) * (s . l)) - ((z . l) * p)) + (((z . l) * p) - (t * p))).|| is V11() real ext-real Element of REAL

((z . l) * ((s . l) - p)) + (((z . l) * p) - (t * p)) is Element of the carrier of X

||.(((z . l) * ((s . l) - p)) + (((z . l) * p) - (t * p))).|| is V11() real ext-real Element of REAL

((z . l) - t) * p is Element of the carrier of X

((z . l) * ((s . l) - p)) + (((z . l) - t) * p) is Element of the carrier of X

||.(((z . l) * ((s . l) - p)) + (((z . l) - t) * p)).|| is V11() real ext-real Element of REAL

||.(((z . l) - t) * p).|| is V11() real ext-real Element of REAL

||.((z . l) * ((s . l) - p)).|| + ||.(((z . l) - t) * p).|| is V11() real ext-real Element of REAL

k * (n / (||.p.|| + k)) is V11() real ext-real Element of REAL

||.p.|| * ||.((z . l) - t).|| is V11() real ext-real Element of REAL

||.p.|| * (n / (||.p.|| + k)) is V11() real ext-real Element of REAL

(k * (n / (||.p.|| + k))) + (||.p.|| * (n / (||.p.|| + k))) is V11() real ext-real Element of REAL

(n / (||.p.|| + k)) * (||.p.|| + k) is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

||.z.|| is V11() real ext-real Element of REAL

t is Element of the carrier of X

z * t is Element of the carrier of X

k is Element of the carrier of X

p is V11() real ext-real Element of REAL

||.z.|| + 1 is V11() real ext-real Element of REAL

0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

p / (||.z.|| + 1) is V11() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(z * s) . n is Element of the carrier of X

((z * s) . n) - k is Element of the carrier of X

||.(((z * s) . n) - k).|| is V11() real ext-real Element of REAL

s . n is Element of the carrier of X

(s . n) - t is Element of the carrier of X

||.((s . n) - t).|| is V11() real ext-real Element of REAL

z * ((s . n) - t) is Element of the carrier of X

||.(z * ((s . n) - t)).|| is V11() real ext-real Element of REAL

||.z.|| * ||.((s . n) - t).|| is V11() real ext-real Element of REAL

0 + ||.z.|| is V11() real ext-real Element of REAL

(||.z.|| + 1) * (p / (||.z.|| + 1)) is V11() real ext-real Element of REAL

||.z.|| * (p / (||.z.|| + 1)) is V11() real ext-real Element of REAL

(z * s) . n is Element of the carrier of X

((z * s) . n) - k is Element of the carrier of X

||.(((z * s) . n) - k).|| is V11() real ext-real Element of REAL

z * (s . n) is Element of the carrier of X

(z * (s . n)) - (z * t) is Element of the carrier of X

||.((z * (s . n)) - (z * t)).|| is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

s * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

||.z.|| is V11() real ext-real Element of REAL

t is Element of the carrier of X

t * z is Element of the carrier of X

k is Element of the carrier of X

p is V11() real ext-real Element of REAL

||.z.|| + 1 is V11() real ext-real Element of REAL

0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

p / (||.z.|| + 1) is V11() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(s * z) . n is Element of the carrier of X

((s * z) . n) - k is Element of the carrier of X

||.(((s * z) . n) - k).|| is V11() real ext-real Element of REAL

s . n is Element of the carrier of X

(s . n) - t is Element of the carrier of X

||.((s . n) - t).|| is V11() real ext-real Element of REAL

((s . n) - t) * z is Element of the carrier of X

||.(((s . n) - t) * z).|| is V11() real ext-real Element of REAL

||.((s . n) - t).|| * ||.z.|| is V11() real ext-real Element of REAL

0 + ||.z.|| is V11() real ext-real Element of REAL

(p / (||.z.|| + 1)) * (||.z.|| + 1) is V11() real ext-real Element of REAL

(p / (||.z.|| + 1)) * ||.z.|| is V11() real ext-real Element of REAL

(s * z) . n is Element of the carrier of X

((s * z) . n) - k is Element of the carrier of X

||.(((s * z) . n) - k).|| is V11() real ext-real Element of REAL

(s . n) * z is Element of the carrier of X

((s . n) * z) - (t * z) is Element of the carrier of X

||.(((s . n) * z) - (t * z)).|| is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim (z * s) is Element of the carrier of X

lim s is Element of the carrier of X

z * (lim s) is Element of the carrier of X

||.z.|| is V11() real ext-real Element of REAL

||.z.|| + 1 is V11() real ext-real Element of REAL

0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

p is V11() real ext-real Element of REAL

p / (||.z.|| + 1) is V11() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s . k is Element of the carrier of X

(s . k) - (lim s) is Element of the carrier of X

||.((s . k) - (lim s)).|| is V11() real ext-real Element of REAL

||.z.|| * ||.((s . k) - (lim s)).|| is V11() real ext-real Element of REAL

||.z.|| * (p / (||.z.|| + 1)) is V11() real ext-real Element of REAL

z * ((s . k) - (lim s)) is Element of the carrier of X

||.(z * ((s . k) - (lim s))).|| is V11() real ext-real Element of REAL

(z * s) . k is Element of the carrier of X

((z * s) . k) - (z * (lim s)) is Element of the carrier of X

||.(((z * s) . k) - (z * (lim s))).|| is V11() real ext-real Element of REAL

z * (s . k) is Element of the carrier of X

(z * (s . k)) - (z * (lim s)) is Element of the carrier of X

||.((z * (s . k)) - (z * (lim s))).|| is V11() real ext-real Element of REAL

0 + ||.z.|| is V11() real ext-real Element of REAL

(||.z.|| + 1) * (p / (||.z.|| + 1)) is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

s * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim (s * z) is Element of the carrier of X

lim s is Element of the carrier of X

(lim s) * z is Element of the carrier of X

||.z.|| is V11() real ext-real Element of REAL

||.z.|| + 1 is V11() real ext-real Element of REAL

0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

p is V11() real ext-real Element of REAL

p / (||.z.|| + 1) is V11() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s . k is Element of the carrier of X

(s . k) - (lim s) is Element of the carrier of X

||.((s . k) - (lim s)).|| is V11() real ext-real Element of REAL

||.((s . k) - (lim s)).|| * ||.z.|| is V11() real ext-real Element of REAL

(p / (||.z.|| + 1)) * ||.z.|| is V11() real ext-real Element of REAL

((s . k) - (lim s)) * z is Element of the carrier of X

||.(((s . k) - (lim s)) * z).|| is V11() real ext-real Element of REAL

(s * z) . k is Element of the carrier of X

((s * z) . k) - ((lim s) * z) is Element of the carrier of X

||.(((s * z) . k) - ((lim s) * z)).|| is V11() real ext-real Element of REAL

(s . k) * z is Element of the carrier of X

((s . k) * z) - ((lim s) * z) is Element of the carrier of X

||.(((s . k) * z) - ((lim s) * z)).|| is V11() real ext-real Element of REAL

0 + ||.z.|| is V11() real ext-real Element of REAL

(p / (||.z.|| + 1)) * (||.z.|| + 1) is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim z is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim (z * s) is Element of the carrier of X

lim s is Element of the carrier of X

(lim z) * (lim s) is Element of the carrier of X

||.z.|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

t is V11() real ext-real set

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z . n is Element of the carrier of X

||.(z . n).|| is V11() real ext-real Element of REAL

||.z.|| . n is V11() real ext-real Element of REAL

z . 1 is Element of the carrier of X

||.(z . 1).|| is V11() real ext-real Element of REAL

||.z.|| . 1 is V11() real ext-real Element of REAL

||.(lim s).|| is V11() real ext-real Element of REAL

n is V11() real ext-real Element of REAL

||.(lim s).|| + n is V11() real ext-real Element of REAL

0 + 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

k is V11() real ext-real Element of REAL

k / (||.(lim s).|| + n) is V11() real ext-real Element of REAL

n4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

n4 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z . l is Element of the carrier of X

(z . l) - (lim z) is Element of the carrier of X

||.((z . l) - (lim z)).|| is V11() real ext-real Element of REAL

||.(lim s).|| * ||.((z . l) - (lim z)).|| is V11() real ext-real Element of REAL

||.(lim s).|| * (k / (||.(lim s).|| + n)) is V11() real ext-real Element of REAL

((z . l) - (lim z)) * (lim s) is Element of the carrier of X

||.(((z . l) - (lim z)) * (lim s)).|| is V11() real ext-real Element of REAL

||.(z . l).|| is V11() real ext-real Element of REAL

(z * s) . l is Element of the carrier of X

((z * s) . l) - ((lim z) * (lim s)) is Element of the carrier of X

||.(((z * s) . l) - ((lim z) * (lim s))).|| is V11() real ext-real Element of REAL

s . l is Element of the carrier of X

(z . l) * (s . l) is Element of the carrier of X

((z . l) * (s . l)) - ((lim z) * (lim s)) is Element of the carrier of X

||.(((z . l) * (s . l)) - ((lim z) * (lim s))).|| is V11() real ext-real Element of REAL

(z . l) * (lim s) is Element of the carrier of X

((z . l) * (s . l)) - ((z . l) * (lim s)) is Element of the carrier of X

((z . l) * (lim s)) - ((lim z) * (lim s)) is Element of the carrier of X

(((z . l) * (s . l)) - ((z . l) * (lim s))) + (((z . l) * (lim s)) - ((lim z) * (lim s))) is Element of the carrier of X

||.((((z . l) * (s . l)) - ((z . l) * (lim s))) + (((z . l) * (lim s)) - ((lim z) * (lim s)))).|| is V11() real ext-real Element of REAL

(s . l) - (lim s) is Element of the carrier of X

(z . l) * ((s . l) - (lim s)) is Element of the carrier of X

((z . l) * ((s . l) - (lim s))) + (((z . l) * (lim s)) - ((lim z) * (lim s))) is Element of the carrier of X

||.(((z . l) * ((s . l) - (lim s))) + (((z . l) * (lim s)) - ((lim z) * (lim s)))).|| is V11() real ext-real Element of REAL

((z . l) * ((s . l) - (lim s))) + (((z . l) - (lim z)) * (lim s)) is Element of the carrier of X

||.(((z . l) * ((s . l) - (lim s))) + (((z . l) - (lim z)) * (lim s))).|| is V11() real ext-real Element of REAL

||.((z . l) * ((s . l) - (lim s))).|| is V11() real ext-real Element of REAL

||.((z . l) * ((s . l) - (lim s))).|| + ||.(((z . l) - (lim z)) * (lim s)).|| is V11() real ext-real Element of REAL

||.((s . l) - (lim s)).|| is V11() real ext-real Element of REAL

||.(z . l).|| * ||.((s . l) - (lim s)).|| is V11() real ext-real Element of REAL

n * (k / (||.(lim s).|| + n)) is V11() real ext-real Element of REAL

(n * (k / (||.(lim s).|| + n))) + (||.(lim s).|| * (k / (||.(lim s).|| + n))) is V11() real ext-real Element of REAL

(k / (||.(lim s).|| + n)) * (||.(lim s).|| + n) is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

z * s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

Partial_Sums (z * s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

Partial_Sums s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

z * (Partial_Sums s) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

s * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

Partial_Sums (s * z) is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

(Partial_Sums s) * z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums (s * z)) . t is Element of the carrier of X

((Partial_Sums s) * z) . t is Element of the carrier of X

t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums (s * z)) . (t + 1) is Element of the carrier of X

(s * z) . (t + 1) is Element of the carrier of X

((Partial_Sums (s * z)) . t) + ((s * z) . (t + 1)) is Element of the carrier of X

(Partial_Sums s) . t is Element of the carrier of X

((Partial_Sums s) . t) * z is Element of the carrier of X

(((Partial_Sums s) . t) * z) + ((s * z) . (t + 1)) is Element of the carrier of X

s . (t + 1) is Element of the carrier of X

(s . (t + 1)) * z is Element of the carrier of X

(((Partial_Sums s) . t) * z) + ((s . (t + 1)) * z) is Element of the carrier of X

((Partial_Sums s) . t) + (s . (t + 1)) is Element of the carrier of X

(((Partial_Sums s) . t) + (s . (t + 1))) * z is Element of the carrier of X

(Partial_Sums s) . (t + 1) is Element of the carrier of X

((Partial_Sums s) . (t + 1)) * z is Element of the carrier of X

((Partial_Sums s) * z) . (t + 1) is Element of the carrier of X

(Partial_Sums (s * z)) . 0 is Element of the carrier of X

(s * z) . 0 is Element of the carrier of X

s . 0 is Element of the carrier of X

(s . 0) * z is Element of the carrier of X

(Partial_Sums s) . 0 is Element of the carrier of X

((Partial_Sums s) . 0) * z is Element of the carrier of X

((Partial_Sums s) * z) . 0 is Element of the carrier of X

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums (z * s)) . t is Element of the carrier of X

(z * (Partial_Sums s)) . t is Element of the carrier of X

t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums (z * s)) . (t + 1) is Element of the carrier of X

(z * s) . (t + 1) is Element of the carrier of X

((Partial_Sums (z * s)) . t) + ((z * s) . (t + 1)) is Element of the carrier of X

(Partial_Sums s) . t is Element of the carrier of X

z * ((Partial_Sums s) . t) is Element of the carrier of X

(z * ((Partial_Sums s) . t)) + ((z * s) . (t + 1)) is Element of the carrier of X

s . (t + 1) is Element of the carrier of X

z * (s . (t + 1)) is Element of the carrier of X

(z * ((Partial_Sums s) . t)) + (z * (s . (t + 1))) is Element of the carrier of X

((Partial_Sums s) . t) + (s . (t + 1)) is Element of the carrier of X

z * (((Partial_Sums s) . t) + (s . (t + 1))) is Element of the carrier of X

(Partial_Sums s) . (t + 1) is Element of the carrier of X

z * ((Partial_Sums s) . (t + 1)) is Element of the carrier of X

(z * (Partial_Sums s)) . (t + 1) is Element of the carrier of X

(Partial_Sums (z * s)) . 0 is Element of the carrier of X

(z * s) . 0 is Element of the carrier of X

s . 0 is Element of the carrier of X

z * (s . 0) is Element of the carrier of X

(Partial_Sums s) . 0 is Element of the carrier of X

z * ((Partial_Sums s) . 0) is Element of the carrier of X

(z * (Partial_Sums s)) . 0 is Element of the carrier of X

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

Partial_Sums s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

(Partial_Sums s) . z is Element of the carrier of X

||.((Partial_Sums s) . z).|| is V11() real ext-real Element of REAL

||.s.|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

Partial_Sums ||.s.|| is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(Partial_Sums ||.s.||) . z is V11() real ext-real Element of REAL

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums s) . t is Element of the carrier of X

||.((Partial_Sums s) . t).|| is V11() real ext-real Element of REAL

(Partial_Sums ||.s.||) . t is V11() real ext-real Element of REAL

t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s . (t + 1) is Element of the carrier of X

||.(s . (t + 1)).|| is V11() real ext-real Element of REAL

||.((Partial_Sums s) . t).|| + ||.(s . (t + 1)).|| is V11() real ext-real Element of REAL

((Partial_Sums ||.s.||) . t) + ||.(s . (t + 1)).|| is V11() real ext-real Element of REAL

((Partial_Sums s) . t) + (s . (t + 1)) is Element of the carrier of X

||.(((Partial_Sums s) . t) + (s . (t + 1))).|| is V11() real ext-real Element of REAL

(Partial_Sums s) . (t + 1) is Element of the carrier of X

||.((Partial_Sums s) . (t + 1)).|| is V11() real ext-real Element of REAL

||.s.|| . (t + 1) is V11() real ext-real Element of REAL

((Partial_Sums ||.s.||) . t) + (||.s.|| . (t + 1)) is V11() real ext-real Element of REAL

(Partial_Sums ||.s.||) . (t + 1) is V11() real ext-real Element of REAL

(Partial_Sums ||.s.||) . 0 is V11() real ext-real Element of REAL

||.s.|| . 0 is V11() real ext-real Element of REAL

s . 0 is Element of the carrier of X

||.(s . 0).|| is V11() real ext-real Element of REAL

(Partial_Sums s) . 0 is Element of the carrier of X

||.((Partial_Sums s) . 0).|| is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

Partial_Sums s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

(Partial_Sums s) . z is Element of the carrier of X

t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

Partial_Sums t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

(Partial_Sums t) . z is Element of the carrier of X

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums s) . k is Element of the carrier of X

(Partial_Sums t) . k is Element of the carrier of X

k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums s) . (k + 1) is Element of the carrier of X

(Partial_Sums t) . (k + 1) is Element of the carrier of X

s . (k + 1) is Element of the carrier of X

((Partial_Sums t) . k) + (s . (k + 1)) is Element of the carrier of X

t . (k + 1) is Element of the carrier of X

((Partial_Sums t) . k) + (t . (k + 1)) is Element of the carrier of X

(Partial_Sums s) . 0 is Element of the carrier of X

(Partial_Sums t) . 0 is Element of the carrier of X

s . 0 is Element of the carrier of X

t . 0 is Element of the carrier of X

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

0. X is V82(X) Element of the carrier of X

z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim z is Element of the carrier of X

s is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

lim s is V11() real ext-real Element of REAL

t is V11() real ext-real set

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s . p is V11() real ext-real Element of REAL

(s . p) - 0 is V11() real ext-real Element of REAL

abs ((s . p) - 0) is V11() real ext-real Element of REAL

z . p is Element of the carrier of X

(z . p) - (0. X) is Element of the carrier of X

||.((z . p) - (0. X)).|| is V11() real ext-real Element of REAL

||.(z . p).|| is V11() real ext-real Element of REAL

abs (s . p) is V11() real ext-real Element of REAL

t is V11() real ext-real Element of REAL

X is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

z is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s . k is Element of the carrier of X

t . k is Element of the carrier of X

z #N k is Element of the carrier of X

z GeoSeq is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

(z GeoSeq) . k is Element of the carrier of X

k ! is V11() real ext-real Element of REAL

1 / (k !) is V11() real ext-real Element of REAL

(1 / (k !)) * (z #N k) is Element of the carrier of X

F

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 V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z is set

s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

CHK (s,X) is V11() real ext-real Element of COMPLEX

F

t is V11() real ext-real Element of REAL

t * F

0 * F

k is set

1 * F

p is set

z is Relation-like Function-like set

dom z is set

s is set

z . s is set

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

F

s is V1() Relation-like NAT -defined the carrier of F

t is V1() Relation-like NAT -defined the carrier of F

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

t . k is Element of the carrier of F

F

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

F

X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X -' 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X - 1 is V11() real ext-real Element of REAL

(X - 1) + 1 is V11() real ext-real Element of REAL

X ! is V11() real ext-real Element of REAL

(X -' 1) ! is V11() real ext-real Element of REAL

((X -' 1) !) * X is V11() real ext-real Element of REAL

z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X + 1) -' z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X + 1) - z is V11() real ext-real Element of REAL

X - z is V11() real ext-real Element of REAL

(X - z) + 1 is V11() real ext-real Element of REAL

X -' z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X -' z) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

((X + 1) -' z) ! is V11() real ext-real Element of REAL

(X -' z) ! is V11() real ext-real Element of REAL

((X -' z) !) * ((X -' z) + 1) is V11() real ext-real Element of REAL

((X -' z) !) * ((X - z) + 1) is V11() real ext-real Element of REAL

((X -' z) !) * ((X + 1) - z) is V11() real ext-real Element of REAL

X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X -' 1) ! is V11() real ext-real Element of REAL

((X -' 1) !) * X is V11() real ext-real Element of REAL

X ! is V11() real ext-real Element of REAL

s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z -' s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(z -' s) ! is V11() real ext-real Element of REAL

z + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(z + 1) - s is V11() real ext-real Element of REAL

((z -' s) !) * ((z + 1) - s) is V11() real ext-real Element of REAL

(z + 1) -' s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

((z + 1) -' s) ! is V11() real ext-real Element of REAL

X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X ! is V11() real ext-real Element of REAL

z is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

s is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z . t is V11() real ext-real Element of REAL

t ! is V11() real ext-real Element of REAL

X -' t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X -' t) ! is V11() real ext-real Element of REAL

(t !) * ((X -' t) !) is V11() real ext-real Element of REAL

(X !) / ((t !) * ((X -' t) !)) is V11() real ext-real Element of REAL

s . t is V11() real ext-real Element of REAL

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z . t is V11() real ext-real Element of REAL

s . t is V11() real ext-real Element of REAL

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

s is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z . t is V11() real ext-real Element of REAL

t ! is V11() real ext-real Element of REAL

X -' t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X -' t) ! is V11() real ext-real Element of REAL

(t !) * ((X -' t) !) is V11() real ext-real Element of REAL

1 / ((t !) * ((X -' t) !)) is V11() real ext-real Element of REAL

s . t is V11() real ext-real Element of REAL

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z . t is V11() real ext-real Element of REAL

s . t is V11() real ext-real Element of REAL

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

X is non empty ZeroStr

the carrier of X is V1() set

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

0. X is V82(X) Element of the carrier of X

z is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

s . 0 is Element of the carrier of X

t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

t + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s . (t + 1) is Element of the carrier of X

z . t is Element of the carrier of X

s is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

s . 0 is Element of the carrier of X

t is V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

t . 0 is Element of the carrier of X

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s . k is Element of the carrier of X

t . k is Element of the carrier of X

k + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s . (k + 1) is Element of the carrier of X

t . (k + 1) is Element of the carrier of X

z . k is Element of the carrier of X

z is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of z is V1() set

K7(NAT, the carrier of z) is set

K6(K7(NAT, the carrier of z)) is set

X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s is Element of the carrier of z

(X) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

t is Element of the carrier of z

0. z is V82(z) Element of the carrier of z

k is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))

p is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

k . n is Element of the carrier of z

s #N n is Element of the carrier of z

s GeoSeq is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))

(s GeoSeq) . n is Element of the carrier of z

(X) . n is V11() real ext-real Element of REAL

((X) . n) * (s #N n) is Element of the carrier of z

X -' n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

t #N (X -' n) is Element of the carrier of z

t GeoSeq is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))

(t GeoSeq) . (X -' n) is Element of the carrier of z

(((X) . n) * (s #N n)) * (t #N (X -' n)) is Element of the carrier of z

p . n is Element of the carrier of z

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

k . n is Element of the carrier of z

p . n is Element of the carrier of z

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

z is non empty right_complementable V126() V127() V128() V129() V130() V131() V132() V136() V137() RealNormSpace-like V153() V156() V160() V161() V162() V163() V165() V175() Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr

the carrier of z is V1() set

K7(NAT, the carrier of z) is set

K6(K7(NAT, the carrier of z)) is set

X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

s is Element of the carrier of z

(X) is V1() Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

t is Element of the carrier of z

0. z is V82(z) Element of the carrier of z

k is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))

p is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

k . n is Element of the carrier of z

s #N n is Element of the carrier of z

s GeoSeq is V1() Relation-like NAT -defined the carrier of z -valued Function-like V26( NAT ) V30( NAT , the carrier of z) Element of K6(K7(NAT, the carrier of z))

(s GeoSeq) . n is Element of the carrier of z

(X) . n is V11() real ext-real Element of REAL

((X) . n) * (s #N n) is Element of the carrier of z

X -' n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT

t