:: LOPBAN_3 semantic presentation

REAL is V4() V47() V52() V53() V54() V58() set

NAT is V4() epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() Element of K32(REAL)

K32(REAL) is V4() set

COMPLEX is V4() V47() V52() V58() set

RAT is V4() V47() V52() V53() V54() V55() V58() set

INT is V4() V47() V52() V53() V54() V55() V56() V58() set

K33(COMPLEX,COMPLEX) is V4() complex-valued set

K32(K33(COMPLEX,COMPLEX)) is V4() set

K33(K33(COMPLEX,COMPLEX),COMPLEX) is V4() complex-valued set

K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is V4() set

K33(REAL,REAL) is V4() complex-valued ext-real-valued real-valued set

K32(K33(REAL,REAL)) is V4() set

K33(K33(REAL,REAL),REAL) is V4() complex-valued ext-real-valued real-valued set

K32(K33(K33(REAL,REAL),REAL)) is V4() set

K33(RAT,RAT) is V4() RAT -valued complex-valued ext-real-valued real-valued set

K32(K33(RAT,RAT)) is V4() set

K33(K33(RAT,RAT),RAT) is V4() RAT -valued complex-valued ext-real-valued real-valued set

K32(K33(K33(RAT,RAT),RAT)) is V4() set

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

K32(K33(INT,INT)) is V4() set

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

K32(K33(K33(INT,INT),INT)) is V4() set

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

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

K32(K33(K33(NAT,NAT),NAT)) is V4() set

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

K32(K33(NAT,REAL)) is V4() set

omega is V4() epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() set

K32(omega) is V4() set

K32(NAT) is V4() set

K390() is V4() set

K33(K390(),K390()) is V4() set

K33(K33(K390(),K390()),K390()) is V4() set

K32(K33(K33(K390(),K390()),K390())) is V4() set

K33(REAL,K390()) is V4() set

K33(K33(REAL,K390()),K390()) is V4() set

K32(K33(K33(REAL,K390()),K390())) is V4() set

K396() is RLSStruct

the carrier of K396() is set

K32( the carrier of K396()) is V4() set

K400() is Element of K32( the carrier of K396())

K33(K400(),K400()) is set

K33(K33(K400(),K400()),REAL) is complex-valued ext-real-valued real-valued set

K32(K33(K33(K400(),K400()),REAL)) is V4() set

the_set_of_l1RealSequences is Element of K32( the carrier of K396())

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

K32(K33(the_set_of_l1RealSequences,REAL)) is V4() set

0c is V4() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() set

1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

0 is V4() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() Element of NAT

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

K32(K33(NAT,NAT)) is V4() set

2 is V4() epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

X is non empty right_complementable add-associative right_zeroed NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

0. X is V79(X) right_complementable Element of the carrier of X

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

Partial_Sums x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

(Partial_Sums x) . seq is right_complementable Element of the carrier of X

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . y is right_complementable Element of the carrier of X

(Partial_Sums x) . y is right_complementable Element of the carrier of X

y + 1 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . (y + 1) is right_complementable Element of the carrier of X

(Partial_Sums x) . (y + 1) is right_complementable Element of the carrier of X

(0. X) + (x . (y + 1)) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(0. X),(x . (y + 1))) is right_complementable Element of the carrier of X

[(0. X),(x . (y + 1))] is set

the addF of X . [(0. X),(x . (y + 1))] is set

((Partial_Sums x) . y) + (x . (y + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . y),(x . (y + 1))) is right_complementable Element of the carrier of X

[((Partial_Sums x) . y),(x . (y + 1))] is set

the addF of X . [((Partial_Sums x) . y),(x . (y + 1))] is set

x . 0 is right_complementable Element of the carrier of X

(Partial_Sums x) . 0 is right_complementable Element of the carrier of X

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

0. X is V79(X) right_complementable Element of the carrier of X

NAT --> (0. X) is V4() Relation-like NAT -defined the carrier of X -valued Function-like constant V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

Partial_Sums x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is V24() real ext-real Element of REAL

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

(Partial_Sums x) . y is right_complementable Element of the carrier of X

((Partial_Sums x) . y) - (0. X) is right_complementable Element of the carrier of X

- (0. X) is right_complementable Element of the carrier of X

((Partial_Sums x) . y) + (- (0. X)) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,((Partial_Sums x) . y),(- (0. X))) is right_complementable Element of the carrier of X

[((Partial_Sums x) . y),(- (0. X))] is set

the addF of X . [((Partial_Sums x) . y),(- (0. X))] is set

||.(((Partial_Sums x) . y) - (0. X)).|| is V24() real ext-real non negative Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . n is right_complementable Element of the carrier of X

(0. X) - (0. X) is right_complementable Element of the carrier of X

(0. X) + (- (0. X)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(0. X),(- (0. X))) is right_complementable Element of the carrier of X

[(0. X),(- (0. X))] is set

the addF of X . [(0. X),(- (0. X))] is set

||.((0. X) - (0. X)).|| is V24() real ext-real non negative Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

Partial_Sums x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

lim (Partial_Sums x) is right_complementable Element of the carrier of X

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

||.x.|| is V4() Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(NAT,REAL))

seq is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

||.x.|| . seq is V24() real ext-real Element of REAL

x . seq is right_complementable Element of the carrier of X

||.(x . seq).|| is V24() real ext-real non negative Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

x is right_complementable Element of the carrier of X

seq is right_complementable Element of the carrier of X

x - seq is right_complementable Element of the carrier of X

- seq is right_complementable Element of the carrier of X

x + (- seq) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,x,(- seq)) is right_complementable Element of the carrier of X

[x,(- seq)] is set

the addF of X . [x,(- seq)] is set

||.(x - seq).|| is V24() real ext-real non negative Element of REAL

y is right_complementable Element of the carrier of X

x - y is right_complementable Element of the carrier of X

- y is right_complementable Element of the carrier of X

x + (- y) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,x,(- y)) is right_complementable Element of the carrier of X

[x,(- y)] is set

the addF of X . [x,(- y)] is set

y - seq is right_complementable Element of the carrier of X

y + (- seq) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,y,(- seq)) is right_complementable Element of the carrier of X

[y,(- seq)] is set

the addF of X . [y,(- seq)] is set

(x - y) + (y - seq) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x - y),(y - seq)) is right_complementable Element of the carrier of X

[(x - y),(y - seq)] is set

the addF of X . [(x - y),(y - seq)] is set

||.((x - y) + (y - seq)).|| is V24() real ext-real non negative Element of REAL

0. X is V79(X) right_complementable Element of the carrier of X

x - (0. X) is right_complementable Element of the carrier of X

- (0. X) is right_complementable Element of the carrier of X

x + (- (0. X)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,x,(- (0. X))) is right_complementable Element of the carrier of X

[x,(- (0. X))] is set

the addF of X . [x,(- (0. X))] is set

(x - (0. X)) - seq is right_complementable Element of the carrier of X

(x - (0. X)) + (- seq) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x - (0. X)),(- seq)) is right_complementable Element of the carrier of X

[(x - (0. X)),(- seq)] is set

the addF of X . [(x - (0. X)),(- seq)] is set

||.((x - (0. X)) - seq).|| is V24() real ext-real non negative Element of REAL

y - y is right_complementable Element of the carrier of X

y + (- y) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,y,(- y)) is right_complementable Element of the carrier of X

[y,(- y)] is set

the addF of X . [y,(- y)] is set

x - (y - y) is right_complementable Element of the carrier of X

- (y - y) is right_complementable Element of the carrier of X

x + (- (y - y)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,x,(- (y - y))) is right_complementable Element of the carrier of X

[x,(- (y - y))] is set

the addF of X . [x,(- (y - y))] is set

(x - (y - y)) - seq is right_complementable Element of the carrier of X

(x - (y - y)) + (- seq) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x - (y - y)),(- seq)) is right_complementable Element of the carrier of X

[(x - (y - y)),(- seq)] is set

the addF of X . [(x - (y - y)),(- seq)] is set

||.((x - (y - y)) - seq).|| is V24() real ext-real non negative Element of REAL

(x - y) + y is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x - y),y) is right_complementable Element of the carrier of X

[(x - y),y] is set

the addF of X . [(x - y),y] is set

((x - y) + y) - seq is right_complementable Element of the carrier of X

((x - y) + y) + (- seq) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((x - y) + y),(- seq)) is right_complementable Element of the carrier of X

[((x - y) + y),(- seq)] is set

the addF of X . [((x - y) + y),(- seq)] is set

||.(((x - y) + y) - seq).|| is V24() real ext-real non negative Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is right_complementable Element of the carrier of X

y is V24() real ext-real Element of REAL

y / 2 is V24() real ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

yn is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . yn is right_complementable Element of the carrier of X

(x . yn) - seq is right_complementable Element of the carrier of X

- seq is right_complementable Element of the carrier of X

(x . yn) + (- seq) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(x . yn),(- seq)) is right_complementable Element of the carrier of X

[(x . yn),(- seq)] is set

the addF of X . [(x . yn),(- seq)] is set

||.((x . yn) - seq).|| is V24() real ext-real non negative Element of REAL

x . n is right_complementable Element of the carrier of X

seq - (x . n) is right_complementable Element of the carrier of X

- (x . n) is right_complementable Element of the carrier of X

seq + (- (x . n)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,seq,(- (x . n))) is right_complementable Element of the carrier of X

[seq,(- (x . n))] is set

the addF of X . [seq,(- (x . n))] is set

((x . yn) - seq) + (seq - (x . n)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((x . yn) - seq),(seq - (x . n))) is right_complementable Element of the carrier of X

[((x . yn) - seq),(seq - (x . n))] is set

the addF of X . [((x . yn) - seq),(seq - (x . n))] is set

||.(((x . yn) - seq) + (seq - (x . n))).|| is V24() real ext-real non negative Element of REAL

||.(seq - (x . n)).|| is V24() real ext-real non negative Element of REAL

||.((x . yn) - seq).|| + ||.(seq - (x . n)).|| is V24() real ext-real non negative Element of REAL

(x . yn) - (x . n) is right_complementable Element of the carrier of X

(x . yn) + (- (x . n)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . yn),(- (x . n))) is right_complementable Element of the carrier of X

[(x . yn),(- (x . n))] is set

the addF of X . [(x . yn),(- (x . n))] is set

||.((x . yn) - (x . n)).|| is V24() real ext-real non negative Element of REAL

(x . n) - seq is right_complementable Element of the carrier of X

(x . n) + (- seq) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . n),(- seq)) is right_complementable Element of the carrier of X

[(x . n),(- seq)] is set

the addF of X . [(x . n),(- seq)] is set

||.((x . n) - seq).|| is V24() real ext-real non negative Element of REAL

(y / 2) + (y / 2) is V24() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is V24() real ext-real Element of REAL

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

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . y is right_complementable Element of the carrier of X

n is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

yn is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . yn is right_complementable Element of the carrier of X

(x . yn) - (x . y) is right_complementable Element of the carrier of X

- (x . y) is right_complementable Element of the carrier of X

(x . yn) + (- (x . y)) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(x . yn),(- (x . y))) is right_complementable Element of the carrier of X

[(x . yn),(- (x . y))] is set

the addF of X . [(x . yn),(- (x . y))] is set

||.((x . yn) - (x . y)).|| is V24() real ext-real non negative Element of REAL

(x . y) - (x . yn) is right_complementable Element of the carrier of X

- (x . yn) is right_complementable Element of the carrier of X

(x . y) + (- (x . yn)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . y),(- (x . yn))) is right_complementable Element of the carrier of X

[(x . y),(- (x . yn))] is set

the addF of X . [(x . y),(- (x . yn))] is set

||.((x . y) - (x . yn)).|| is V24() real ext-real non negative Element of REAL

x . n is right_complementable Element of the carrier of X

(x . n) - (x . y) is right_complementable Element of the carrier of X

(x . n) + (- (x . y)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . n),(- (x . y))) is right_complementable Element of the carrier of X

[(x . n),(- (x . y))] is set

the addF of X . [(x . n),(- (x . y))] is set

||.((x . n) - (x . y)).|| is V24() real ext-real non negative Element of REAL

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

||.((x . n) - (x . y)).|| + ||.((x . y) - (x . yn)).|| is V24() real ext-real non negative Element of REAL

((x . n) - (x . y)) + ((x . y) - (x . yn)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((x . n) - (x . y)),((x . y) - (x . yn))) is right_complementable Element of the carrier of X

[((x . n) - (x . y)),((x . y) - (x . yn))] is set

the addF of X . [((x . n) - (x . y)),((x . y) - (x . yn))] is set

||.(((x . n) - (x . y)) + ((x . y) - (x . yn))).|| is V24() real ext-real non negative Element of REAL

(x . n) - (x . yn) is right_complementable Element of the carrier of X

(x . n) + (- (x . yn)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . n),(- (x . yn))) is right_complementable Element of the carrier of X

[(x . n),(- (x . yn))] is set

the addF of X . [(x . n),(- (x . yn))] is set

||.((x . n) - (x . yn)).|| is V24() real ext-real non negative Element of REAL

seq is V24() real ext-real Element of REAL

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . y is right_complementable Element of the carrier of X

n is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . n is right_complementable Element of the carrier of X

(x . n) - (x . y) is right_complementable Element of the carrier of X

- (x . y) is right_complementable Element of the carrier of X

(x . n) + (- (x . y)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . n),(- (x . y))) is right_complementable Element of the carrier of X

[(x . n),(- (x . y))] is set

the addF of X . [(x . n),(- (x . y))] is set

||.((x . n) - (x . y)).|| is V24() real ext-real non negative Element of REAL

seq is V24() real ext-real Element of REAL

y is V24() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

0. X is V79(X) right_complementable Element of the carrier of X

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

||.x.|| is V4() Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(NAT,REAL))

Partial_Sums ||.x.|| is V4() Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(NAT,REAL))

seq is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

(Partial_Sums ||.x.||) . seq is V24() real ext-real Element of REAL

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

||.x.|| . y is V24() real ext-real Element of REAL

(Partial_Sums ||.x.||) . y is V24() real ext-real Element of REAL

y + 1 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

||.x.|| . (y + 1) is V24() real ext-real Element of REAL

(Partial_Sums ||.x.||) . (y + 1) is V24() real ext-real Element of REAL

||.(0. X).|| is V4() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() Element of REAL

||.(0. X).|| + (||.x.|| . (y + 1)) is V24() real ext-real Element of REAL

x . y is right_complementable Element of the carrier of X

||.(x . y).|| is V24() real ext-real non negative Element of REAL

||.(x . y).|| + (||.x.|| . (y + 1)) is V24() real ext-real Element of REAL

((Partial_Sums ||.x.||) . y) + (||.x.|| . (y + 1)) is V24() real ext-real Element of REAL

||.x.|| . 0 is V24() real ext-real Element of REAL

(Partial_Sums ||.x.||) . 0 is V24() real ext-real Element of REAL

||.x.|| . seq is V24() real ext-real Element of REAL

x . seq is right_complementable Element of the carrier of X

||.(x . seq).|| is V24() real ext-real non negative Element of REAL

||.(0. X).|| is V4() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

seq is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is right_complementable Element of the carrier of X

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

yn is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq . k is right_complementable Element of the carrier of X

(seq . k) - y is right_complementable Element of the carrier of X

- y is right_complementable Element of the carrier of X

(seq . k) + (- y) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(seq . k),(- y)) is right_complementable Element of the carrier of X

[(seq . k),(- y)] is set

the addF of X . [(seq . k),(- y)] is set

||.((seq . k) - y).|| is V24() real ext-real non negative Element of REAL

l is V4() Relation-like NAT -defined NAT -valued Function-like V29( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K32(K33(NAT,NAT))

x * l is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of x

l . k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . (l . k) is right_complementable Element of the carrier of X

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

seq is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

lim seq is right_complementable Element of the carrier of X

lim x is right_complementable Element of the carrier of X

y is V4() Relation-like NAT -defined NAT -valued Function-like V29( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K32(K33(NAT,NAT))

x * y is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of x

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

yn is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

y . k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq . k is right_complementable Element of the carrier of X

x . (y . k) is right_complementable Element of the carrier of X

(seq . k) - (lim x) is right_complementable Element of the carrier of X

- (lim x) is right_complementable Element of the carrier of X

(seq . k) + (- (lim x)) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(seq . k),(- (lim x))) is right_complementable Element of the carrier of X

[(seq . k),(- (lim x))] is set

the addF of X . [(seq . k),(- (lim x))] is set

||.((seq . k) - (lim x)).|| is V24() real ext-real non negative Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x ^\ y is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of x

lim (x ^\ y) is right_complementable Element of the carrier of X

lim x is right_complementable Element of the carrier of X

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq ^\ y is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of seq

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq ^\ y is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of seq

n is right_complementable Element of the carrier of X

yn is V24() real ext-real Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k + y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

l is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq . l is right_complementable Element of the carrier of X

(seq . l) - n is right_complementable Element of the carrier of X

- n is right_complementable Element of the carrier of X

(seq . l) + (- n) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(seq . l),(- n)) is right_complementable Element of the carrier of X

[(seq . l),(- n)] is set

the addF of X . [(seq . l),(- n)] is set

||.((seq . l) - n).|| is V24() real ext-real non negative Element of REAL

l is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real set

(k + y) + l is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

l - y is V24() real ext-real Element of REAL

m1 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k + m1 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

(k + m1) + y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

- y is V24() real ext-real Element of REAL

((k + m1) + y) + (- y) is V24() real ext-real Element of REAL

m1 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

m1 + y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . m1 is right_complementable Element of the carrier of X

(x . m1) - n is right_complementable Element of the carrier of X

(x . m1) + (- n) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . m1),(- n)) is right_complementable Element of the carrier of X

[(x . m1),(- n)] is set

the addF of X . [(x . m1),(- n)] is set

||.((x . m1) - n).|| is V24() real ext-real non negative Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

lim seq is right_complementable Element of the carrier of X

lim x is right_complementable Element of the carrier of X

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq ^\ y is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of seq

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq ^\ y is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of seq

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

yn is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

yn + y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

l is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real set

(yn + y) + l is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

k - y is V24() real ext-real Element of REAL

l is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

yn + l is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

(yn + l) + y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

- y is V24() real ext-real Element of REAL

((yn + l) + y) + (- y) is V24() real ext-real Element of REAL

m1 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

m1 + y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . m1 is right_complementable Element of the carrier of X

(x . m1) - (lim x) is right_complementable Element of the carrier of X

- (lim x) is right_complementable Element of the carrier of X

(x . m1) + (- (lim x)) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(x . m1),(- (lim x))) is right_complementable Element of the carrier of X

[(x . m1),(- (lim x))] is set

the addF of X . [(x . m1),(- (lim x))] is set

||.((x . m1) - (lim x)).|| is V24() real ext-real non negative Element of REAL

seq . k is right_complementable Element of the carrier of X

(seq . k) - (lim x) is right_complementable Element of the carrier of X

(seq . k) + (- (lim x)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(seq . k),(- (lim x))) is right_complementable Element of the carrier of X

[(seq . k),(- (lim x))] is set

the addF of X . [(seq . k),(- (lim x))] is set

||.((seq . k) - (lim x)).|| is V24() real ext-real non negative Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq ^\ n is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of seq

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is right_complementable Element of the carrier of X

y is right_complementable Element of the carrier of X

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

yn is V4() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . k is right_complementable Element of the carrier of X

(x . k) - y is right_complementable Element of the carrier of X

- y is right_complementable Element of the carrier of X

(x . k) + (- y) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(x . k),(- y)) is right_complementable Element of the carrier of X

[(x . k),(- y)] is set

the addF of X . [(x . k),(- y)] is set

||.((x . k) - y).|| is V24() real ext-real non negative Element of REAL

seq - y is right_complementable Element of the carrier of X

seq + (- y) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,seq,(- y)) is right_complementable Element of the carrier of X

[seq,(- y)] is set

the addF of X . [seq,(- y)] is set

||.(seq - y).|| is V24() real ext-real non negative Element of REAL

0. X is V79(X) right_complementable Element of the carrier of X

||.(0. X).|| is V4() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

0. X is V79(X) right_complementable Element of the carrier of X

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

||.x.|| is V4() Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(NAT,REAL))

Partial_Sums ||.x.|| is V4() Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(NAT,REAL))

seq is V24() real ext-real set

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

(Partial_Sums ||.x.||) . y is V24() real ext-real Element of REAL

((Partial_Sums ||.x.||) . y) - 0 is V24() real ext-real Element of REAL

abs (((Partial_Sums ||.x.||) . y) - 0) is V24() real ext-real Element of REAL

0 - 0 is V4() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() Element of REAL

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

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

0. X is V79(X) right_complementable Element of the carrier of X

NAT --> (0. X) is V4() Relation-like NAT -defined the carrier of X -valued Function-like constant V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

x . seq is right_complementable Element of the carrier of X

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

0. X is V79(X) right_complementable Element of the carrier of X

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

lim x is right_complementable Element of the carrier of X

Partial_Sums x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(Partial_Sums x) ^\ 1 is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of Partial_Sums x

lim ((Partial_Sums x) ^\ 1) is right_complementable Element of the carrier of X

lim (Partial_Sums x) is right_complementable Element of the carrier of X

((Partial_Sums x) ^\ 1) - (Partial_Sums x) is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

lim (((Partial_Sums x) ^\ 1) - (Partial_Sums x)) is right_complementable Element of the carrier of X

(lim (Partial_Sums x)) - (lim (Partial_Sums x)) is right_complementable Element of the carrier of X

- (lim (Partial_Sums x)) is right_complementable Element of the carrier of X

(lim (Partial_Sums x)) + (- (lim (Partial_Sums x))) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,(lim (Partial_Sums x)),(- (lim (Partial_Sums x)))) is right_complementable Element of the carrier of X

[(lim (Partial_Sums x)),(- (lim (Partial_Sums x)))] is set

the addF of X . [(lim (Partial_Sums x)),(- (lim (Partial_Sums x)))] is set

seq is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

seq + 1 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

(Partial_Sums x) . (seq + 1) is right_complementable Element of the carrier of X

(Partial_Sums x) . seq is right_complementable Element of the carrier of X

x . (seq + 1) is right_complementable Element of the carrier of X

((Partial_Sums x) . seq) + (x . (seq + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . seq),(x . (seq + 1))) is right_complementable Element of the carrier of X

[((Partial_Sums x) . seq),(x . (seq + 1))] is set

the addF of X . [((Partial_Sums x) . seq),(x . (seq + 1))] is set

x ^\ 1 is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of x

(x ^\ 1) . seq is right_complementable Element of the carrier of X

((Partial_Sums x) . seq) + ((x ^\ 1) . seq) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . seq),((x ^\ 1) . seq)) is right_complementable Element of the carrier of X

[((Partial_Sums x) . seq),((x ^\ 1) . seq)] is set

the addF of X . [((Partial_Sums x) . seq),((x ^\ 1) . seq)] is set

((Partial_Sums x) ^\ 1) . seq is right_complementable Element of the carrier of X

((x ^\ 1) . seq) + ((Partial_Sums x) . seq) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((x ^\ 1) . seq),((Partial_Sums x) . seq)) is right_complementable Element of the carrier of X

[((x ^\ 1) . seq),((Partial_Sums x) . seq)] is set

the addF of X . [((x ^\ 1) . seq),((Partial_Sums x) . seq)] is set

(((Partial_Sums x) ^\ 1) . seq) - ((Partial_Sums x) . seq) is right_complementable Element of the carrier of X

- ((Partial_Sums x) . seq) is right_complementable Element of the carrier of X

(((Partial_Sums x) ^\ 1) . seq) + (- ((Partial_Sums x) . seq)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(((Partial_Sums x) ^\ 1) . seq),(- ((Partial_Sums x) . seq))) is right_complementable Element of the carrier of X

[(((Partial_Sums x) ^\ 1) . seq),(- ((Partial_Sums x) . seq))] is set

the addF of X . [(((Partial_Sums x) ^\ 1) . seq),(- ((Partial_Sums x) . seq))] is set

((Partial_Sums x) . seq) - ((Partial_Sums x) . seq) is right_complementable Element of the carrier of X

((Partial_Sums x) . seq) + (- ((Partial_Sums x) . seq)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . seq),(- ((Partial_Sums x) . seq))) is right_complementable Element of the carrier of X

[((Partial_Sums x) . seq),(- ((Partial_Sums x) . seq))] is set

the addF of X . [((Partial_Sums x) . seq),(- ((Partial_Sums x) . seq))] is set

((x ^\ 1) . seq) + (((Partial_Sums x) . seq) - ((Partial_Sums x) . seq)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((x ^\ 1) . seq),(((Partial_Sums x) . seq) - ((Partial_Sums x) . seq))) is right_complementable Element of the carrier of X

[((x ^\ 1) . seq),(((Partial_Sums x) . seq) - ((Partial_Sums x) . seq))] is set

the addF of X . [((x ^\ 1) . seq),(((Partial_Sums x) . seq) - ((Partial_Sums x) . seq))] is set

((x ^\ 1) . seq) + (0. X) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((x ^\ 1) . seq),(0. X)) is right_complementable Element of the carrier of X

[((x ^\ 1) . seq),(0. X)] is set

the addF of X . [((x ^\ 1) . seq),(0. X)] is set

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is V4() set

K32(K33(NAT, the carrier of X)) is V4() set

x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

Partial_Sums x is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

seq is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

Partial_Sums seq is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(Partial_Sums x) + (Partial_Sums seq) is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x + seq is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

Partial_Sums (x + seq) is V4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

y + 1 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT

((Partial_Sums x) + (Partial_Sums seq)) . (y + 1) is right_complementable Element of the carrier of X

(Partial_Sums x) . (y + 1) is right_complementable Element of the carrier of X

(Partial_Sums seq) . (y + 1) is right_complementable Element of the carrier of X

((Partial_Sums x) . (y + 1)) + ((Partial_Sums seq) . (y + 1)) is right_complementable Element of the carrier of X

the addF of X is V4() Relation-like K33( the carrier of X, the carrier of X) -defined the carrier of X -valued Function-like V29(K33( the carrier of X, the carrier of X)) V30(K33( the carrier of X, the carrier of X), the carrier of X) Element of K32(K33(K33( the carrier of X, the carrier of X), the carrier of X))

K33( the carrier of X, the carrier of X) is V4() set

K33(K33( the carrier of X, the carrier of X), the carrier of X) is V4() set

K32(K33(K33( the carrier of X, the carrier of X), the carrier of X)) is V4() set

K411( the carrier of X, the addF of X,((Partial_Sums x) . (y + 1)),((Partial_Sums seq) . (y + 1))) is right_complementable Element of the carrier of X

[((Partial_Sums x) . (y + 1)),((Partial_Sums seq) . (y + 1))] is set

the addF of X . [((Partial_Sums x) . (y + 1)),((Partial_Sums seq) . (y + 1))] is set

(Partial_Sums x) . y is right_complementable Element of the carrier of X

x . (y + 1) is right_complementable Element of the carrier of X

((Partial_Sums x) . y) + (x . (y + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . y),(x . (y + 1))) is right_complementable Element of the carrier of X

[((Partial_Sums x) . y),(x . (y + 1))] is set

the addF of X . [((Partial_Sums x) . y),(x . (y + 1))] is set

(((Partial_Sums x) . y) + (x . (y + 1))) + ((Partial_Sums seq) . (y + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(((Partial_Sums x) . y) + (x . (y + 1))),((Partial_Sums seq) . (y + 1))) is right_complementable Element of the carrier of X

[(((Partial_Sums x) . y) + (x . (y + 1))),((Partial_Sums seq) . (y + 1))] is set

the addF of X . [(((Partial_Sums x) . y) + (x . (y + 1))),((Partial_Sums seq) . (y + 1))] is set

seq . (y + 1) is right_complementable Element of the carrier of X

(Partial_Sums seq) . y is right_complementable Element of the carrier of X

(seq . (y + 1)) + ((Partial_Sums seq) . y) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(seq . (y + 1)),((Partial_Sums seq) . y)) is right_complementable Element of the carrier of X

[(seq . (y + 1)),((Partial_Sums seq) . y)] is set

the addF of X . [(seq . (y + 1)),((Partial_Sums seq) . y)] is set

(((Partial_Sums x) . y) + (x . (y + 1))) + ((seq . (y + 1)) + ((Partial_Sums seq) . y)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(((Partial_Sums x) . y) + (x . (y + 1))),((seq . (y + 1)) + ((Partial_Sums seq) . y))) is right_complementable Element of the carrier of X

[(((Partial_Sums x) . y) + (x . (y + 1))),((seq . (y + 1)) + ((Partial_Sums seq) . y))] is set

the addF of X . [(((Partial_Sums x) . y) + (x . (y + 1))),((seq . (y + 1)) + ((Partial_Sums seq) . y))] is set

(((Partial_Sums x) . y) + (x . (y + 1))) + (seq . (y + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(((Partial_Sums x) . y) + (x . (y + 1))),(seq . (y + 1))) is right_complementable Element of the carrier of X

[(((Partial_Sums x) . y) + (x . (y + 1))),(seq . (y + 1))] is set

the addF of X . [(((Partial_Sums x) . y) + (x . (y + 1))),(seq . (y + 1))] is set

((((Partial_Sums x) . y) + (x . (y + 1))) + (seq . (y + 1))) + ((Partial_Sums seq) . y) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((((Partial_Sums x) . y) + (x . (y + 1))) + (seq . (y + 1))),((Partial_Sums seq) . y)) is right_complementable Element of the carrier of X

[((((Partial_Sums x) . y) + (x . (y + 1))) + (seq . (y + 1))),((Partial_Sums seq) . y)] is set

the addF of X . [((((Partial_Sums x) . y) + (x . (y + 1))) + (seq . (y + 1))),((Partial_Sums seq) . y)] is set

(x . (y + 1)) + (seq . (y + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . (y + 1)),(seq . (y + 1))) is right_complementable Element of the carrier of X

[(x . (y + 1)),(seq . (y + 1))] is set

the addF of X . [(x . (y + 1)),(seq . (y + 1))] is set

((Partial_Sums x) . y) + ((x . (y + 1)) + (seq . (y + 1))) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . y),((x . (y + 1)) + (seq . (y + 1)))) is right_complementable Element of the carrier of X

[((Partial_Sums x) . y),((x . (y + 1)) + (seq . (y + 1)))] is set

the addF of X . [((Partial_Sums x) . y),((x . (y + 1)) + (seq . (y + 1)))] is set

(((Partial_Sums x) . y) + ((x . (y + 1)) + (seq . (y + 1)))) + ((Partial_Sums seq) . y) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(((Partial_Sums x) . y) + ((x . (y + 1)) + (seq . (y + 1)))),((Partial_Sums seq) . y)) is right_complementable Element of the carrier of X

[(((Partial_Sums x) . y) + ((x . (y + 1)) + (seq . (y + 1)))),((Partial_Sums seq) . y)] is set

the addF of X . [(((Partial_Sums x) . y) + ((x . (y + 1)) + (seq . (y + 1)))),((Partial_Sums seq) . y)] is set

(x + seq) . (y + 1) is right_complementable Element of the carrier of X

((Partial_Sums x) . y) + ((x + seq) . (y + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . y),((x + seq) . (y + 1))) is right_complementable Element of the carrier of X

[((Partial_Sums x) . y),((x + seq) . (y + 1))] is set

the addF of X . [((Partial_Sums x) . y),((x + seq) . (y + 1))] is set

(((Partial_Sums x) . y) + ((x + seq) . (y + 1))) + ((Partial_Sums seq) . y) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(((Partial_Sums x) . y) + ((x + seq) . (y + 1))),((Partial_Sums seq) . y)) is right_complementable Element of the carrier of X

[(((Partial_Sums x) . y) + ((x + seq) . (y + 1))),((Partial_Sums seq) . y)] is set

the addF of X . [(((Partial_Sums x) . y) + ((x + seq) . (y + 1))),((Partial_Sums seq) . y)] is set

((Partial_Sums x) . y) + ((Partial_Sums seq) . y) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . y),((Partial_Sums seq) . y)) is right_complementable Element of the carrier of X

[((Partial_Sums x) . y),((Partial_Sums seq) . y)] is set

the addF of X . [((Partial_Sums x) . y),((Partial_Sums seq) . y)] is set

(((Partial_Sums x) . y) + ((Partial_Sums seq) . y)) + ((x + seq) . (y + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(((Partial_Sums x) . y) + ((Partial_Sums seq) . y)),((x + seq) . (y + 1))) is right_complementable Element of the carrier of X

[(((Partial_Sums x) . y) + ((Partial_Sums seq) . y)),((x + seq) . (y + 1))] is set

the addF of X . [(((Partial_Sums x) . y) + ((Partial_Sums seq) . y)),((x + seq) . (y + 1))] is set

((Partial_Sums x) + (Partial_Sums seq)) . y is right_complementable Element of the carrier of X

(((Partial_Sums x) + (Partial_Sums seq)) . y) + ((x + seq) . (y + 1)) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(((Partial_Sums x) + (Partial_Sums seq)) . y),((x + seq) . (y + 1))) is right_complementable Element of the carrier of X

[(((Partial_Sums x) + (Partial_Sums seq)) . y),((x + seq) . (y + 1))] is set

the addF of X . [(((Partial_Sums x) + (Partial_Sums seq)) . y),((x + seq) . (y + 1))] is set

((Partial_Sums x) + (Partial_Sums seq)) . 0 is right_complementable Element of the carrier of X

(Partial_Sums x) . 0 is right_complementable Element of the carrier of X

(Partial_Sums seq) . 0 is right_complementable Element of the carrier of X

((Partial_Sums x) . 0) + ((Partial_Sums seq) . 0) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,((Partial_Sums x) . 0),((Partial_Sums seq) . 0)) is right_complementable Element of the carrier of X

[((Partial_Sums x) . 0),((Partial_Sums seq) . 0)] is set

the addF of X . [((Partial_Sums x) . 0),((Partial_Sums seq) . 0)] is set

x . 0 is right_complementable Element of the carrier of X

(x . 0) + ((Partial_Sums seq) . 0) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . 0),((Partial_Sums seq) . 0)) is right_complementable Element of the carrier of X

[(x . 0),((Partial_Sums seq) . 0)] is set

the addF of X . [(x . 0),((Partial_Sums seq) . 0)] is set

seq . 0 is right_complementable Element of the carrier of X

(x . 0) + (seq . 0) is right_complementable Element of the carrier of X

K411( the carrier of X, the addF of X,(x . 0),(seq . 0)) is right_complementable Element of the carrier of X

[(x . 0),(seq . 0)] is set

the addF of X . [(x . 0),(seq . 0)] is set

(x + seq) . 0 is right_complementable Element of the carrier of X

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like NORMSTR

the carrier of X is V4() set