:: BHSP_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(COMPLEX,COMPLEX) is complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative integer V59() V60() V61() V62() V63() V64() V65() set
1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer 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 integer V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
- 1 is V11() real ext-real non positive integer Element of REAL
2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq is non empty addLoopStr
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X . 0 is Element of the carrier of Rseq
seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq . 0 is Element of the carrier of Rseq
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . (n + 1) is Element of the carrier of Rseq
seq . n is Element of the carrier of Rseq
X . (n + 1) is Element of the carrier of Rseq
(seq . n) + (X . (n + 1)) is Element of the carrier of Rseq
seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq . 0 is Element of the carrier of Rseq
n is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n . 0 is Element of the carrier of Rseq
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . k is Element of the carrier of Rseq
n . k is Element of the carrier of Rseq
k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . (k + 1) is Element of the carrier of Rseq
n . (k + 1) is Element of the carrier of Rseq
X . (k + 1) is Element of the carrier of Rseq
(n . k) + (X . (k + 1)) is Element of the carrier of Rseq
Rseq is non empty Abelian add-associative addLoopStr
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) + (Rseq,seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X + seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,(X + seq)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
((Rseq,X) + (Rseq,seq)) . (k + 1) is Element of the carrier of Rseq
(Rseq,X) . (k + 1) is Element of the carrier of Rseq
(Rseq,seq) . (k + 1) is Element of the carrier of Rseq
((Rseq,X) . (k + 1)) + ((Rseq,seq) . (k + 1)) is Element of the carrier of Rseq
(Rseq,X) . k is Element of the carrier of Rseq
X . (k + 1) is Element of the carrier of Rseq
((Rseq,X) . k) + (X . (k + 1)) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) + ((Rseq,seq) . (k + 1)) is Element of the carrier of Rseq
seq . (k + 1) is Element of the carrier of Rseq
(Rseq,seq) . k is Element of the carrier of Rseq
(seq . (k + 1)) + ((Rseq,seq) . k) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) + ((seq . (k + 1)) + ((Rseq,seq) . k)) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) + (seq . (k + 1)) is Element of the carrier of Rseq
((((Rseq,X) . k) + (X . (k + 1))) + (seq . (k + 1))) + ((Rseq,seq) . k) is Element of the carrier of Rseq
(X . (k + 1)) + (seq . (k + 1)) is Element of the carrier of Rseq
((Rseq,X) . k) + ((X . (k + 1)) + (seq . (k + 1))) is Element of the carrier of Rseq
(((Rseq,X) . k) + ((X . (k + 1)) + (seq . (k + 1)))) + ((Rseq,seq) . k) is Element of the carrier of Rseq
(X + seq) . (k + 1) is Element of the carrier of Rseq
((Rseq,X) . k) + ((X + seq) . (k + 1)) is Element of the carrier of Rseq
(((Rseq,X) . k) + ((X + seq) . (k + 1))) + ((Rseq,seq) . k) is Element of the carrier of Rseq
((Rseq,X) . k) + ((Rseq,seq) . k) is Element of the carrier of Rseq
(((Rseq,X) . k) + ((Rseq,seq) . k)) + ((X + seq) . (k + 1)) is Element of the carrier of Rseq
((Rseq,X) + (Rseq,seq)) . k is Element of the carrier of Rseq
(((Rseq,X) + (Rseq,seq)) . k) + ((X + seq) . (k + 1)) is Element of the carrier of Rseq
((Rseq,X) + (Rseq,seq)) . 0 is Element of the carrier of Rseq
(Rseq,X) . 0 is Element of the carrier of Rseq
(Rseq,seq) . 0 is Element of the carrier of Rseq
((Rseq,X) . 0) + ((Rseq,seq) . 0) is Element of the carrier of Rseq
X . 0 is Element of the carrier of Rseq
(X . 0) + ((Rseq,seq) . 0) is Element of the carrier of Rseq
seq . 0 is Element of the carrier of Rseq
(X . 0) + (seq . 0) is Element of the carrier of Rseq
(X + seq) . 0 is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed zeroed addLoopStr
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) - (Rseq,seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X - seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,(X - seq)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
((Rseq,X) - (Rseq,seq)) . (k + 1) is Element of the carrier of Rseq
(Rseq,X) . (k + 1) is Element of the carrier of Rseq
(Rseq,seq) . (k + 1) is Element of the carrier of Rseq
((Rseq,X) . (k + 1)) - ((Rseq,seq) . (k + 1)) is Element of the carrier of Rseq
- ((Rseq,seq) . (k + 1)) is Element of the carrier of Rseq
((Rseq,X) . (k + 1)) + (- ((Rseq,seq) . (k + 1))) is Element of the carrier of Rseq
(Rseq,X) . k is Element of the carrier of Rseq
X . (k + 1) is Element of the carrier of Rseq
((Rseq,X) . k) + (X . (k + 1)) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) - ((Rseq,seq) . (k + 1)) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) + (- ((Rseq,seq) . (k + 1))) is Element of the carrier of Rseq
seq . (k + 1) is Element of the carrier of Rseq
(Rseq,seq) . k is Element of the carrier of Rseq
(seq . (k + 1)) + ((Rseq,seq) . k) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) - ((seq . (k + 1)) + ((Rseq,seq) . k)) is Element of the carrier of Rseq
- ((seq . (k + 1)) + ((Rseq,seq) . k)) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) + (- ((seq . (k + 1)) + ((Rseq,seq) . k))) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) - (seq . (k + 1)) is Element of the carrier of Rseq
- (seq . (k + 1)) is Element of the carrier of Rseq
(((Rseq,X) . k) + (X . (k + 1))) + (- (seq . (k + 1))) is Element of the carrier of Rseq
((((Rseq,X) . k) + (X . (k + 1))) - (seq . (k + 1))) - ((Rseq,seq) . k) is Element of the carrier of Rseq
- ((Rseq,seq) . k) is Element of the carrier of Rseq
((((Rseq,X) . k) + (X . (k + 1))) - (seq . (k + 1))) + (- ((Rseq,seq) . k)) is Element of the carrier of Rseq
(X . (k + 1)) - (seq . (k + 1)) is Element of the carrier of Rseq
(X . (k + 1)) + (- (seq . (k + 1))) is Element of the carrier of Rseq
((Rseq,X) . k) + ((X . (k + 1)) - (seq . (k + 1))) is Element of the carrier of Rseq
(((Rseq,X) . k) + ((X . (k + 1)) - (seq . (k + 1)))) - ((Rseq,seq) . k) is Element of the carrier of Rseq
(((Rseq,X) . k) + ((X . (k + 1)) - (seq . (k + 1)))) + (- ((Rseq,seq) . k)) is Element of the carrier of Rseq
((Rseq,X) . k) - ((Rseq,seq) . k) is Element of the carrier of Rseq
((Rseq,X) . k) + (- ((Rseq,seq) . k)) is Element of the carrier of Rseq
(((Rseq,X) . k) - ((Rseq,seq) . k)) + ((X . (k + 1)) - (seq . (k + 1))) is Element of the carrier of Rseq
((Rseq,X) - (Rseq,seq)) . k is Element of the carrier of Rseq
(((Rseq,X) - (Rseq,seq)) . k) + ((X . (k + 1)) - (seq . (k + 1))) is Element of the carrier of Rseq
(X - seq) . (k + 1) is Element of the carrier of Rseq
(((Rseq,X) - (Rseq,seq)) . k) + ((X - seq) . (k + 1)) is Element of the carrier of Rseq
((Rseq,X) - (Rseq,seq)) . 0 is Element of the carrier of Rseq
(Rseq,X) . 0 is Element of the carrier of Rseq
(Rseq,seq) . 0 is Element of the carrier of Rseq
((Rseq,X) . 0) - ((Rseq,seq) . 0) is Element of the carrier of Rseq
- ((Rseq,seq) . 0) is Element of the carrier of Rseq
((Rseq,X) . 0) + (- ((Rseq,seq) . 0)) is Element of the carrier of Rseq
X . 0 is Element of the carrier of Rseq
(X . 0) - ((Rseq,seq) . 0) is Element of the carrier of Rseq
(X . 0) + (- ((Rseq,seq) . 0)) is Element of the carrier of Rseq
seq . 0 is Element of the carrier of Rseq
(X . 0) - (seq . 0) is Element of the carrier of Rseq
- (seq . 0) is Element of the carrier of Rseq
(X . 0) + (- (seq . 0)) is Element of the carrier of Rseq
(X - seq) . 0 is Element of the carrier of Rseq
Rseq is V11() real ext-real Element of REAL
X is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Rseq * seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(Rseq * seq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Rseq * (X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() 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 integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq * (X,seq)) . (k + 1) is Element of the carrier of X
(X,seq) . (k + 1) is Element of the carrier of X
Rseq * ((X,seq) . (k + 1)) is Element of the carrier of X
(X,seq) . k is Element of the carrier of X
seq . (k + 1) is Element of the carrier of X
((X,seq) . k) + (seq . (k + 1)) is Element of the carrier of X
Rseq * (((X,seq) . k) + (seq . (k + 1))) is Element of the carrier of X
Rseq * ((X,seq) . k) is Element of the carrier of X
Rseq * (seq . (k + 1)) is Element of the carrier of X
(Rseq * ((X,seq) . k)) + (Rseq * (seq . (k + 1))) is Element of the carrier of X
(Rseq * (X,seq)) . k is Element of the carrier of X
((Rseq * (X,seq)) . k) + (Rseq * (seq . (k + 1))) is Element of the carrier of X
(Rseq * seq) . (k + 1) is Element of the carrier of X
((Rseq * (X,seq)) . k) + ((Rseq * seq) . (k + 1)) is Element of the carrier of X
(Rseq * (X,seq)) . 0 is Element of the carrier of X
(X,seq) . 0 is Element of the carrier of X
Rseq * ((X,seq) . 0) is Element of the carrier of X
seq . 0 is Element of the carrier of X
Rseq * (seq . 0) is Element of the carrier of X
(Rseq * seq) . 0 is Element of the carrier of X
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
- X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,(- X)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
- (Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(- 1) * X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,((- 1) * X)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(- 1) * (Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
Rseq is V11() real ext-real Element of REAL
X is V11() real ext-real Element of REAL
seq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of seq is V1() set
K7(NAT, the carrier of seq) is set
K6(K7(NAT, the carrier of seq)) is set
n is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
Rseq * (seq,n) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
Rseq * n is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
k is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,k) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
X * (seq,k) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(Rseq * (seq,n)) + (X * (seq,k)) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
X * k is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(Rseq * n) + (X * k) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,((Rseq * n) + (X * k))) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,(Rseq * n)) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,(Rseq * n)) + (X * (seq,k)) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,(X * k)) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,(Rseq * n)) + (seq,(X * k)) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim (Rseq,X) is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim (Rseq,X) is Element of the carrier of Rseq
seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X + seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,(X + seq)) is Element of the carrier of Rseq
(Rseq,(X + seq)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim (Rseq,(X + seq)) is Element of the carrier of Rseq
(Rseq,seq) is Element of the carrier of Rseq
(Rseq,seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim (Rseq,seq) is Element of the carrier of Rseq
(Rseq,X) + (Rseq,seq) is Element of the carrier of Rseq
(Rseq,X) + (Rseq,seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim ((Rseq,X) + (Rseq,seq)) is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim (Rseq,X) is Element of the carrier of Rseq
seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X - seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,(X - seq)) is Element of the carrier of Rseq
(Rseq,(X - seq)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim (Rseq,(X - seq)) is Element of the carrier of Rseq
(Rseq,seq) is Element of the carrier of Rseq
(Rseq,seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim (Rseq,seq) is Element of the carrier of Rseq
(Rseq,X) - (Rseq,seq) is Element of the carrier of Rseq
- (Rseq,seq) is Element of the carrier of Rseq
(Rseq,X) + (- (Rseq,seq)) is Element of the carrier of Rseq
(Rseq,X) - (Rseq,seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim ((Rseq,X) - (Rseq,seq)) is Element of the carrier of Rseq
Rseq is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Rseq * seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(Rseq * seq)) is Element of the carrier of X
(X,(Rseq * seq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (X,(Rseq * seq)) is Element of the carrier of X
(X,seq) is Element of the carrier of X
(X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (X,seq) is Element of the carrier of X
Rseq * (X,seq) is Element of the carrier of X
Rseq * (X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (Rseq * (X,seq)) is Element of the carrier of X
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
0. Rseq is V80(Rseq) Element of the carrier of Rseq
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim X is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . (n + 1) is Element of the carrier of Rseq
(Rseq,X) . n is Element of the carrier of Rseq
X . (n + 1) is Element of the carrier of Rseq
((Rseq,X) . n) + (X . (n + 1)) is Element of the carrier of Rseq
X ^\ 1 is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X
(X ^\ 1) . n is Element of the carrier of Rseq
((Rseq,X) . n) + ((X ^\ 1) . n) is Element of the carrier of Rseq
(Rseq,X) ^\ 1 is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of (Rseq,X)
((Rseq,X) ^\ 1) . n is Element of the carrier of Rseq
(Rseq,X) + (X ^\ 1) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) - (Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(X ^\ 1) + ((Rseq,X) - (Rseq,X)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
K68(((X ^\ 1) + ((Rseq,X) - (Rseq,X))),n) is set
K68((X ^\ 1),n) is set
((X ^\ 1) + ((Rseq,X) - (Rseq,X))) . n is Element of the carrier of Rseq
(X ^\ 1) . n is Element of the carrier of Rseq
((Rseq,X) - (Rseq,X)) . n is Element of the carrier of Rseq
((X ^\ 1) . n) + (((Rseq,X) - (Rseq,X)) . n) is Element of the carrier of Rseq
(Rseq,X) . n is Element of the carrier of Rseq
((Rseq,X) . n) - ((Rseq,X) . n) is Element of the carrier of Rseq
- ((Rseq,X) . n) is Element of the carrier of Rseq
((Rseq,X) . n) + (- ((Rseq,X) . n)) is Element of the carrier of Rseq
((X ^\ 1) . n) + (((Rseq,X) . n) - ((Rseq,X) . n)) is Element of the carrier of Rseq
((X ^\ 1) . n) + H₁(Rseq) is Element of the carrier of Rseq
((Rseq,X) ^\ 1) - (Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
lim ((Rseq,X) ^\ 1) is Element of the carrier of Rseq
lim (Rseq,X) is Element of the carrier of Rseq
lim (((Rseq,X) ^\ 1) - (Rseq,X)) is Element of the carrier of Rseq
(lim (Rseq,X)) - (lim (Rseq,X)) is Element of the carrier of Rseq
- (lim (Rseq,X)) is Element of the carrier of Rseq
(lim (Rseq,X)) + (- (lim (Rseq,X))) is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like V144() UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X . 0 is Element of the carrier of Rseq
X ^\ 1 is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X
(Rseq,(X ^\ 1)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) ^\ 1 is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of (Rseq,X)
seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
((Rseq,X) ^\ 1) - seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(((Rseq,X) ^\ 1) - seq) . (n + 1) is Element of the carrier of Rseq
((Rseq,X) ^\ 1) . (n + 1) is Element of the carrier of Rseq
seq . (n + 1) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . (n + 1)) - (seq . (n + 1)) is Element of the carrier of Rseq
- (seq . (n + 1)) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . (n + 1)) + (- (seq . (n + 1))) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . (n + 1)) - (X . 0) is Element of the carrier of Rseq
- (X . 0) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . (n + 1)) + (- (X . 0)) is Element of the carrier of Rseq
(n + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . ((n + 1) + 1) is Element of the carrier of Rseq
((Rseq,X) . ((n + 1) + 1)) - (X . 0) is Element of the carrier of Rseq
((Rseq,X) . ((n + 1) + 1)) + (- (X . 0)) is Element of the carrier of Rseq
X . ((n + 1) + 1) is Element of the carrier of Rseq
(Rseq,X) . (n + 1) is Element of the carrier of Rseq
(X . ((n + 1) + 1)) + ((Rseq,X) . (n + 1)) is Element of the carrier of Rseq
((X . ((n + 1) + 1)) + ((Rseq,X) . (n + 1))) - (X . 0) is Element of the carrier of Rseq
((X . ((n + 1) + 1)) + ((Rseq,X) . (n + 1))) + (- (X . 0)) is Element of the carrier of Rseq
seq . n is Element of the carrier of Rseq
((X . ((n + 1) + 1)) + ((Rseq,X) . (n + 1))) - (seq . n) is Element of the carrier of Rseq
- (seq . n) is Element of the carrier of Rseq
((X . ((n + 1) + 1)) + ((Rseq,X) . (n + 1))) + (- (seq . n)) is Element of the carrier of Rseq
((Rseq,X) . (n + 1)) - (seq . n) is Element of the carrier of Rseq
((Rseq,X) . (n + 1)) + (- (seq . n)) is Element of the carrier of Rseq
(X . ((n + 1) + 1)) + (((Rseq,X) . (n + 1)) - (seq . n)) is Element of the carrier of Rseq
((Rseq,X) ^\ 1) . n is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . n) - (seq . n) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . n) + (- (seq . n)) is Element of the carrier of Rseq
(X . ((n + 1) + 1)) + ((((Rseq,X) ^\ 1) . n) - (seq . n)) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) - seq) . n is Element of the carrier of Rseq
(X . ((n + 1) + 1)) + ((((Rseq,X) ^\ 1) - seq) . n) is Element of the carrier of Rseq
(X ^\ 1) . (n + 1) is Element of the carrier of Rseq
((((Rseq,X) ^\ 1) - seq) . n) + ((X ^\ 1) . (n + 1)) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) - seq) . 0 is Element of the carrier of Rseq
((Rseq,X) ^\ 1) . 0 is Element of the carrier of Rseq
seq . 0 is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . 0) - (seq . 0) is Element of the carrier of Rseq
- (seq . 0) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . 0) + (- (seq . 0)) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . 0) - (X . 0) is Element of the carrier of Rseq
(((Rseq,X) ^\ 1) . 0) + (- (X . 0)) is Element of the carrier of Rseq
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . (0 + 1) is Element of the carrier of Rseq
((Rseq,X) . (0 + 1)) - (X . 0) is Element of the carrier of Rseq
((Rseq,X) . (0 + 1)) + (- (X . 0)) is Element of the carrier of Rseq
(Rseq,X) . 0 is Element of the carrier of Rseq
X . (0 + 1) is Element of the carrier of Rseq
((Rseq,X) . 0) + (X . (0 + 1)) is Element of the carrier of Rseq
(((Rseq,X) . 0) + (X . (0 + 1))) - (X . 0) is Element of the carrier of Rseq
(((Rseq,X) . 0) + (X . (0 + 1))) + (- (X . 0)) is Element of the carrier of Rseq
(X . (0 + 1)) + (X . 0) is Element of the carrier of Rseq
((X . (0 + 1)) + (X . 0)) - (X . 0) is Element of the carrier of Rseq
((X . (0 + 1)) + (X . 0)) + (- (X . 0)) is Element of the carrier of Rseq
(X . 0) - (X . 0) is Element of the carrier of Rseq
(X . 0) + (- (X . 0)) is Element of the carrier of Rseq
(X . (0 + 1)) + ((X . 0) - (X . 0)) is Element of the carrier of Rseq
0. Rseq is V80(Rseq) Element of the carrier of Rseq
(X . (0 + 1)) + H₁(Rseq) is Element of the carrier of Rseq
(X ^\ 1) . 0 is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X ^\ seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X
seq + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X ^\ (seq + 1) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X
(X ^\ seq) . 0 is Element of the carrier of Rseq
NAT --> ((X ^\ seq) . 0) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() constant V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,(X ^\ seq)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,(X ^\ seq)) ^\ 1 is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of (Rseq,(X ^\ seq))
n is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n . k is Element of the carrier of Rseq
(X ^\ seq) ^\ 1 is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X ^\ seq
(Rseq,((X ^\ seq) ^\ 1)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
((Rseq,(X ^\ seq)) ^\ 1) - n is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X ^\ 0 is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X ^\ seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X
(X ^\ seq) ^\ 1 is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X ^\ seq
(Rseq,((X ^\ seq) ^\ 1)) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . seq is Element of the carrier of Rseq
NAT --> ((Rseq,X) . seq) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() constant V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) ^\ (seq + 1) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of (Rseq,X)
X ^\ (seq + 1) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) subsequence of X
(Rseq,(X ^\ (seq + 1))) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,(X ^\ (seq + 1))) . 0 is Element of the carrier of Rseq
(X ^\ (seq + 1)) . 0 is Element of the carrier of Rseq
0 + (seq + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . (0 + (seq + 1)) is Element of the carrier of Rseq
X . (seq + 1) is Element of the carrier of Rseq
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
((Rseq,X) ^\ (seq + 1)) . k is Element of the carrier of Rseq
(Rseq,(X ^\ (seq + 1))) . k is Element of the carrier of Rseq
n . k is Element of the carrier of Rseq
((Rseq,(X ^\ (seq + 1))) . k) + (n . k) is Element of the carrier of Rseq
k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,(X ^\ (seq + 1))) . (k + 1) is Element of the carrier of Rseq
n . (k + 1) is Element of the carrier of Rseq
((Rseq,(X ^\ (seq + 1))) . (k + 1)) + (n . (k + 1)) is Element of the carrier of Rseq
(X ^\ (seq + 1)) . (k + 1) is Element of the carrier of Rseq
((Rseq,(X ^\ (seq + 1))) . k) + ((X ^\ (seq + 1)) . (k + 1)) is Element of the carrier of Rseq
(n . (k + 1)) + (((Rseq,(X ^\ (seq + 1))) . k) + ((X ^\ (seq + 1)) . (k + 1))) is Element of the carrier of Rseq
(n . (k + 1)) + ((Rseq,(X ^\ (seq + 1))) . k) is Element of the carrier of Rseq
((n . (k + 1)) + ((Rseq,(X ^\ (seq + 1))) . k)) + ((X ^\ (seq + 1)) . (k + 1)) is Element of the carrier of Rseq
((Rseq,X) . seq) + ((Rseq,(X ^\ (seq + 1))) . k) is Element of the carrier of Rseq
(((Rseq,X) . seq) + ((Rseq,(X ^\ (seq + 1))) . k)) + ((X ^\ (seq + 1)) . (k + 1)) is Element of the carrier of Rseq
(((Rseq,X) ^\ (seq + 1)) . k) + ((X ^\ (seq + 1)) . (k + 1)) is Element of the carrier of Rseq
k + (seq + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . (k + (seq + 1)) is Element of the carrier of Rseq
((Rseq,X) . (k + (seq + 1))) + ((X ^\ (seq + 1)) . (k + 1)) is Element of the carrier of Rseq
(k + 1) + (seq + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . ((k + 1) + (seq + 1)) is Element of the carrier of Rseq
((Rseq,X) . (k + (seq + 1))) + (X . ((k + 1) + (seq + 1))) is Element of the carrier of Rseq
(k + (seq + 1)) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . ((k + (seq + 1)) + 1) is Element of the carrier of Rseq
(Rseq,X) . ((k + 1) + (seq + 1)) is Element of the carrier of Rseq
((Rseq,X) ^\ (seq + 1)) . (k + 1) is Element of the carrier of Rseq
((Rseq,X) ^\ (seq + 1)) . 0 is Element of the carrier of Rseq
(Rseq,X) . (0 + (seq + 1)) is Element of the carrier of Rseq
((Rseq,X) . seq) + (X . (seq + 1)) is Element of the carrier of Rseq
n . 0 is Element of the carrier of Rseq
((Rseq,(X ^\ (seq + 1))) . 0) + (n . 0) is Element of the carrier of Rseq
(Rseq,(X ^\ (seq + 1))) + n is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,((X ^\ seq) ^\ 1)) + n is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . seq is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X,0) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . 0 is Element of the carrier of Rseq
X . 0 is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X,1) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . 1 is Element of the carrier of Rseq
(Rseq,X,0) is Element of the carrier of Rseq
(Rseq,X) . 0 is Element of the carrier of Rseq
X . 1 is Element of the carrier of Rseq
(Rseq,X,0) + (X . 1) is Element of the carrier of Rseq
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . (0 + 1) is Element of the carrier of Rseq
((Rseq,X) . 0) + (X . (0 + 1)) is Element of the carrier of Rseq
((Rseq,X) . 0) + (X . 1) is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X,1) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . 1 is Element of the carrier of Rseq
X . 0 is Element of the carrier of Rseq
X . 1 is Element of the carrier of Rseq
(X . 0) + (X . 1) is Element of the carrier of Rseq
(Rseq,X,0) is Element of the carrier of Rseq
(Rseq,X) . 0 is Element of the carrier of Rseq
(Rseq,X,0) + (X . 1) is Element of the carrier of Rseq
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Rseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,seq,(Rseq + 1)) is Element of the carrier of X
(X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) . (Rseq + 1) is Element of the carrier of X
(X,seq,Rseq) is Element of the carrier of X
(X,seq) . Rseq is Element of the carrier of X
seq . (Rseq + 1) is Element of the carrier of X
(X,seq,Rseq) + (seq . (Rseq + 1)) is Element of the carrier of X
Rseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq . (Rseq + 1) is Element of the carrier of X
(X,seq,(Rseq + 1)) is Element of the carrier of X
(X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) . (Rseq + 1) is Element of the carrier of X
(X,seq,Rseq) is Element of the carrier of X
(X,seq) . Rseq is Element of the carrier of X
(X,seq,(Rseq + 1)) - (X,seq,Rseq) is Element of the carrier of X
- (X,seq,Rseq) is Element of the carrier of X
(X,seq,(Rseq + 1)) + (- (X,seq,Rseq)) is Element of the carrier of X
(seq . (Rseq + 1)) + (X,seq,Rseq) is Element of the carrier of X
((seq . (Rseq + 1)) + (X,seq,Rseq)) - (X,seq,Rseq) is Element of the carrier of X
((seq . (Rseq + 1)) + (X,seq,Rseq)) + (- (X,seq,Rseq)) is Element of the carrier of X
(X,seq,Rseq) - (X,seq,Rseq) is Element of the carrier of X
(X,seq,Rseq) + (- (X,seq,Rseq)) is Element of the carrier of X
(seq . (Rseq + 1)) + ((X,seq,Rseq) - (X,seq,Rseq)) is Element of the carrier of X
0. X is V80(X) Element of the carrier of X
(seq . (Rseq + 1)) + (0. X) is Element of the carrier of X
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X . 1 is Element of the carrier of Rseq
(Rseq,X,1) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . 1 is Element of the carrier of Rseq
(Rseq,X,0) is Element of the carrier of Rseq
(Rseq,X) . 0 is Element of the carrier of Rseq
(Rseq,X,1) - (Rseq,X,0) is Element of the carrier of Rseq
- (Rseq,X,0) is Element of the carrier of Rseq
(Rseq,X,1) + (- (Rseq,X,0)) is Element of the carrier of Rseq
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . (0 + 1) is Element of the carrier of Rseq
(Rseq,X,(0 + 1)) is Element of the carrier of Rseq
(Rseq,X) . (0 + 1) is Element of the carrier of Rseq
(Rseq,X,(0 + 1)) - (Rseq,X,0) is Element of the carrier of Rseq
(Rseq,X,(0 + 1)) + (- (Rseq,X,0)) is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,seq) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . seq is Element of the carrier of Rseq
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,n) is Element of the carrier of Rseq
(Rseq,X) . n is Element of the carrier of Rseq
(Rseq,X,seq) - (Rseq,X,n) is Element of the carrier of Rseq
- (Rseq,X,n) is Element of the carrier of Rseq
(Rseq,X,seq) + (- (Rseq,X,n)) is Element of the carrier of Rseq
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X,1,0) is Element of the carrier of Rseq
(Rseq,X,1) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . 1 is Element of the carrier of Rseq
(Rseq,X,0) is Element of the carrier of Rseq
(Rseq,X) . 0 is Element of the carrier of Rseq
(Rseq,X,1) - (Rseq,X,0) is Element of the carrier of Rseq
- (Rseq,X,0) is Element of the carrier of Rseq
(Rseq,X,1) + (- (Rseq,X,0)) is Element of the carrier of Rseq
X . 1 is Element of the carrier of Rseq
X . 0 is Element of the carrier of Rseq
(X . 0) + (X . 1) is Element of the carrier of Rseq
((X . 0) + (X . 1)) - (Rseq,X,0) is Element of the carrier of Rseq
((X . 0) + (X . 1)) + (- (Rseq,X,0)) is Element of the carrier of Rseq
(X . 1) + (X . 0) is Element of the carrier of Rseq
((X . 1) + (X . 0)) - (X . 0) is Element of the carrier of Rseq
- (X . 0) is Element of the carrier of Rseq
((X . 1) + (X . 0)) + (- (X . 0)) is Element of the carrier of Rseq
(X . 0) - (X . 0) is Element of the carrier of Rseq
(X . 0) + (- (X . 0)) is Element of the carrier of Rseq
(X . 1) + ((X . 0) - (X . 0)) is Element of the carrier of Rseq
0. Rseq is V80(Rseq) Element of the carrier of Rseq
(X . 1) + H₁(Rseq) is Element of the carrier of Rseq
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Rseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,seq,(Rseq + 1),Rseq) is Element of the carrier of X
(X,seq,(Rseq + 1)) is Element of the carrier of X
(X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) . (Rseq + 1) is Element of the carrier of X
(X,seq,Rseq) is Element of the carrier of X
(X,seq) . Rseq is Element of the carrier of X
(X,seq,(Rseq + 1)) - (X,seq,Rseq) is Element of the carrier of X
- (X,seq,Rseq) is Element of the carrier of X
(X,seq,(Rseq + 1)) + (- (X,seq,Rseq)) is Element of the carrier of X
seq . (Rseq + 1) is Element of the carrier of X
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like V144() UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is V11() real ext-real Element of REAL
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,k) is Element of the carrier of Rseq
(Rseq,X) . k is Element of the carrier of Rseq
(Rseq,X,m1) is Element of the carrier of Rseq
(Rseq,X) . m1 is Element of the carrier of Rseq
(Rseq,X,k) - (Rseq,X,m1) is Element of the carrier of Rseq
- (Rseq,X,m1) is Element of the carrier of Rseq
(Rseq,X,k) + (- (Rseq,X,m1)) is Element of the carrier of Rseq
||.((Rseq,X,k) - (Rseq,X,m1)).|| is V11() real ext-real Element of REAL
seq is V11() real ext-real Element of REAL
seq is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,k) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . k is Element of the carrier of Rseq
(Rseq,X,m1) is Element of the carrier of Rseq
(Rseq,X) . m1 is Element of the carrier of Rseq
(Rseq,X,k) - (Rseq,X,m1) is Element of the carrier of Rseq
- (Rseq,X,m1) is Element of the carrier of Rseq
(Rseq,X,k) + (- (Rseq,X,m1)) is Element of the carrier of Rseq
||.((Rseq,X,k) - (Rseq,X,m1)).|| is V11() real ext-real Element of REAL
((Rseq,X) . k) - ((Rseq,X) . m1) is Element of the carrier of Rseq
- ((Rseq,X) . m1) is Element of the carrier of Rseq
((Rseq,X) . k) + (- ((Rseq,X) . m1)) is Element of the carrier of Rseq
||.(((Rseq,X) . k) - ((Rseq,X) . m1)).|| is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like V144() UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,k,m1) is Element of the carrier of Rseq
(Rseq,X,k) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . k is Element of the carrier of Rseq
(Rseq,X,m1) is Element of the carrier of Rseq
(Rseq,X) . m1 is Element of the carrier of Rseq
(Rseq,X,k) - (Rseq,X,m1) is Element of the carrier of Rseq
- (Rseq,X,m1) is Element of the carrier of Rseq
(Rseq,X,k) + (- (Rseq,X,m1)) is Element of the carrier of Rseq
||.(Rseq,X,k,m1).|| is V11() real ext-real Element of REAL
seq is V11() real ext-real Element of REAL
seq is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,k,m1) is Element of the carrier of Rseq
(Rseq,X,k) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . k is Element of the carrier of Rseq
(Rseq,X,m1) is Element of the carrier of Rseq
(Rseq,X) . m1 is Element of the carrier of Rseq
(Rseq,X,k) - (Rseq,X,m1) is Element of the carrier of Rseq
- (Rseq,X,m1) is Element of the carrier of Rseq
(Rseq,X,k) + (- (Rseq,X,m1)) is Element of the carrier of Rseq
||.(Rseq,X,k,m1).|| is V11() real ext-real Element of REAL
||.((Rseq,X,k) - (Rseq,X,m1)).|| is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
X + seq is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
||.(X + seq).|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.X.|| + ||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(X + seq).|| . n is V11() real ext-real Element of REAL
(||.X.|| + ||.seq.||) . n is V11() real ext-real Element of REAL
(X + seq) . n is Element of the carrier of Rseq
||.((X + seq) . n).|| is V11() real ext-real Element of REAL
X . n is Element of the carrier of Rseq
seq . n is Element of the carrier of Rseq
(X . n) + (seq . n) is Element of the carrier of Rseq
||.((X . n) + (seq . n)).|| is V11() real ext-real Element of REAL
||.(X . n).|| is V11() real ext-real Element of REAL
||.(seq . n).|| is V11() real ext-real Element of REAL
||.(X . n).|| + ||.(seq . n).|| is V11() real ext-real Element of REAL
||.X.|| . n is V11() real ext-real Element of REAL
(||.X.|| . n) + ||.(seq . n).|| is V11() real ext-real Element of REAL
||.seq.|| . n is V11() real ext-real Element of REAL
(||.X.|| . n) + (||.seq.|| . n) is V11() real ext-real Element of REAL
Rseq is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Rseq * seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.(Rseq * seq).|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
abs Rseq is V11() real ext-real Element of REAL
(abs Rseq) (#) ||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(Rseq * seq).|| . n is V11() real ext-real Element of REAL
((abs Rseq) (#) ||.seq.||) . n is V11() real ext-real Element of REAL
(Rseq * seq) . n is Element of the carrier of X
||.((Rseq * seq) . n).|| is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
Rseq * (seq . n) is Element of the carrier of X
||.(Rseq * (seq . n)).|| is V11() real ext-real Element of REAL
||.(seq . n).|| is V11() real ext-real Element of REAL
(abs Rseq) * ||.(seq . n).|| is V11() real ext-real Element of REAL
||.seq.|| . n is V11() real ext-real Element of REAL
(abs Rseq) * (||.seq.|| . n) is V11() real ext-real Element of REAL
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . n is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
||.(seq . n).|| is V11() real ext-real Element of REAL
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim Rseq is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
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 V80(X) Element of the carrier of X
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . n is V11() real ext-real Element of REAL
Rseq . n is V11() real ext-real Element of REAL
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . (n + 1) is V11() real ext-real Element of REAL
(||.seq.|| . (n + 1)) / (||.seq.|| . n) is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
||.(seq . n).|| is V11() real ext-real Element of REAL
seq . (n + 1) is Element of the carrier of X
||.(seq . (n + 1)).|| is V11() real ext-real Element of REAL
||.(seq . (n + 1)).|| / ||.(seq . n).|| is V11() real ext-real Element of REAL
(||.seq.|| . (n + 1)) / ||.(seq . n).|| is V11() real ext-real Element of REAL
Rseq is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
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 V80(X) Element of the carrier of X
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim seq is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . k is Element of the carrier of X
(seq . k) - H₁(X) is Element of the carrier of X
- (0. X) is Element of the carrier of X
(seq . k) + (- (0. X)) is Element of the carrier of X
||.((seq . k) - H₁(X)).|| is V11() real ext-real Element of REAL
||.(seq . k).|| is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
0. Rseq is V80(Rseq) Element of the carrier of Rseq
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . seq is Element of the carrier of Rseq
||.(X . seq).|| is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . (seq + k) is Element of the carrier of Rseq
||.(X . (seq + k)).|| is V11() real ext-real Element of REAL
k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq + (k + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . (seq + (k + 1)) is Element of the carrier of Rseq
||.(X . (seq + (k + 1))).|| is V11() real ext-real Element of REAL
(seq + k) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . ((seq + k) + 1) is Element of the carrier of Rseq
||.(X . ((seq + k) + 1)).|| is V11() real ext-real Element of REAL
||.(X . ((seq + k) + 1)).|| / ||.(X . (seq + k)).|| is V11() real ext-real Element of REAL
seq + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . (seq + 0) is Element of the carrier of Rseq
||.(X . (seq + 0)).|| is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer set
seq + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . n is Element of the carrier of Rseq
||.(X . n).|| is V11() real ext-real Element of REAL
lim X is Element of the carrier of Rseq
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim Rseq is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
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 V80(X) Element of the carrier of X
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(lim Rseq) - 1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . k is V11() real ext-real Element of REAL
k + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . (k + 1) is Element of the carrier of X
||.(seq . (k + 1)).|| is V11() real ext-real Element of REAL
seq . k is Element of the carrier of X
||.(seq . k).|| is V11() real ext-real Element of REAL
||.(seq . (k + 1)).|| / ||.(seq . k).|| is V11() real ext-real Element of REAL
(||.(seq . (k + 1)).|| / ||.(seq . k).||) - (lim Rseq) is V11() real ext-real Element of REAL
abs ((||.(seq . (k + 1)).|| / ||.(seq . k).||) - (lim Rseq)) is V11() real ext-real Element of REAL
- ((lim Rseq) - 1) is V11() real ext-real Element of REAL
((||.(seq . (k + 1)).|| / ||.(seq . k).||) - (lim Rseq)) + (lim Rseq) is V11() real ext-real Element of REAL
1 - (lim Rseq) is V11() real ext-real Element of REAL
(1 - (lim Rseq)) + (lim Rseq) is V11() real ext-real Element of REAL
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim Rseq is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . n is V11() real ext-real Element of REAL
Rseq . n is V11() real ext-real Element of REAL
n -root (||.seq.|| . n) is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
||.(seq . n).|| is V11() real ext-real Element of REAL
n -root ||.(seq . n).|| is V11() real ext-real Element of REAL
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . k is V11() real ext-real Element of REAL
||.seq.|| . k is V11() real ext-real Element of REAL
k -root (||.seq.|| . k) is V11() real ext-real Element of REAL
seq . k is Element of the carrier of X
||.(seq . k).|| is V11() real ext-real Element of REAL
k -root ||.(seq . k).|| is V11() real ext-real Element of REAL
(k -root ||.(seq . k).||) |^ k is V11() real ext-real Element of REAL
lim seq is Element of the carrier of X
0. X is V80(X) Element of the carrier of X
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim Rseq is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
||.seq.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(lim Rseq) - 1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . k is V11() real ext-real Element of REAL
||.seq.|| . k is V11() real ext-real Element of REAL
k -root (||.seq.|| . k) is V11() real ext-real Element of REAL
seq . k is Element of the carrier of X
||.(seq . k).|| is V11() real ext-real Element of REAL
k -root ||.(seq . k).|| is V11() real ext-real Element of REAL
(k -root ||.(seq . k).||) - (lim Rseq) is V11() real ext-real Element of REAL
abs ((k -root ||.(seq . k).||) - (lim Rseq)) is V11() real ext-real Element of REAL
- ((lim Rseq) - 1) is V11() real ext-real Element of REAL
((k -root ||.(seq . k).||) - (lim Rseq)) + (lim Rseq) is V11() real ext-real Element of REAL
1 - (lim Rseq) is V11() real ext-real Element of REAL
(1 - (lim Rseq)) + (lim Rseq) is V11() real ext-real Element of REAL
(k -root ||.(seq . k).||) |^ k is V11() real ext-real Element of REAL
lim seq is Element of the carrier of X
0. X is V80(X) Element of the carrier of X
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . (seq + 1) is Element of the carrier of Rseq
||.(X . (seq + 1)).|| is V11() real ext-real Element of REAL
||.X.|| . (seq + 1) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . seq is V11() real ext-real Element of REAL
0 + ((Partial_Sums ||.X.||) . seq) is V11() real ext-real Element of REAL
(||.X.|| . (seq + 1)) + ((Partial_Sums ||.X.||) . seq) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . (seq + 1) is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.X.||) . seq is V11() real ext-real Element of REAL
X . 0 is Element of the carrier of Rseq
||.(X . 0).|| is V11() real ext-real Element of REAL
||.X.|| . 0 is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . 0 is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . seq is Element of the carrier of Rseq
||.((Rseq,X) . seq).|| is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . seq is V11() real ext-real Element of REAL
seq + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . (seq + 1) is Element of the carrier of Rseq
||.(X . (seq + 1)).|| is V11() real ext-real Element of REAL
||.((Rseq,X) . seq).|| + ||.(X . (seq + 1)).|| is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . seq) + ||.(X . (seq + 1)).|| is V11() real ext-real Element of REAL
(Rseq,X) . (seq + 1) is Element of the carrier of Rseq
((Rseq,X) . seq) + (X . (seq + 1)) is Element of the carrier of Rseq
||.((Rseq,X) . (seq + 1)).|| is V11() real ext-real Element of REAL
||.X.|| . (seq + 1) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . seq) + (||.X.|| . (seq + 1)) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . (seq + 1) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . 0 is V11() real ext-real Element of REAL
||.X.|| . 0 is V11() real ext-real Element of REAL
X . 0 is Element of the carrier of Rseq
||.(X . 0).|| is V11() real ext-real Element of REAL
(Rseq,X) . 0 is Element of the carrier of Rseq
||.((Rseq,X) . 0).|| is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,seq) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . seq is Element of the carrier of Rseq
||.(Rseq,X,seq).|| is V11() real ext-real Element of REAL
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Sum (||.X.||,seq) is V11() real ext-real Element of REAL
Partial_Sums ||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.X.||) . seq is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . seq is Element of the carrier of Rseq
(Partial_Sums ||.X.||) . seq is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . n is Element of the carrier of Rseq
((Rseq,X) . n) - ((Rseq,X) . seq) is Element of the carrier of Rseq
- ((Rseq,X) . seq) is Element of the carrier of Rseq
((Rseq,X) . n) + (- ((Rseq,X) . seq)) is Element of the carrier of Rseq
||.(((Rseq,X) . n) - ((Rseq,X) . seq)).|| is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . n is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . seq) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . seq)) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(n + m) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . ((n + m) + 1) is Element of the carrier of Rseq
||.(X . ((n + m) + 1)).|| is V11() real ext-real Element of REAL
m + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.X.||) . (n + (m + 1)) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . (n + (m + 1))) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . (n + (m + 1)))) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . (n + (m + 1))) - ((Partial_Sums ||.X.||) . n) is V11() real ext-real Element of REAL
- (((Partial_Sums ||.X.||) . (n + (m + 1))) - ((Partial_Sums ||.X.||) . n)) is V11() real ext-real Element of REAL
abs (- (((Partial_Sums ||.X.||) . (n + (m + 1))) - ((Partial_Sums ||.X.||) . n))) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . ((n + m) + 1) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . ((n + m) + 1)) - ((Partial_Sums ||.X.||) . n) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . ((n + m) + 1)) - ((Partial_Sums ||.X.||) . n)) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . (n + m) is V11() real ext-real Element of REAL
||.X.|| . ((n + m) + 1) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . (n + m)) + (||.X.|| . ((n + m) + 1)) is V11() real ext-real Element of REAL
(((Partial_Sums ||.X.||) . (n + m)) + (||.X.|| . ((n + m) + 1))) - ((Partial_Sums ||.X.||) . n) is V11() real ext-real Element of REAL
abs ((((Partial_Sums ||.X.||) . (n + m)) + (||.X.|| . ((n + m) + 1))) - ((Partial_Sums ||.X.||) . n)) is V11() real ext-real Element of REAL
||.(X . ((n + m) + 1)).|| + ((Partial_Sums ||.X.||) . (n + m)) is V11() real ext-real Element of REAL
(||.(X . ((n + m) + 1)).|| + ((Partial_Sums ||.X.||) . (n + m))) - ((Partial_Sums ||.X.||) . n) is V11() real ext-real Element of REAL
abs ((||.(X . ((n + m) + 1)).|| + ((Partial_Sums ||.X.||) . (n + m))) - ((Partial_Sums ||.X.||) . n)) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . (n + m)) - ((Partial_Sums ||.X.||) . n) is V11() real ext-real Element of REAL
(((Partial_Sums ||.X.||) . (n + m)) - ((Partial_Sums ||.X.||) . n)) + ||.(X . ((n + m) + 1)).|| is V11() real ext-real Element of REAL
abs ((((Partial_Sums ||.X.||) . (n + m)) - ((Partial_Sums ||.X.||) . n)) + ||.(X . ((n + m) + 1)).||) is V11() real ext-real Element of REAL
(Rseq,X) . (n + (m + 1)) is Element of the carrier of Rseq
((Rseq,X) . n) - ((Rseq,X) . (n + (m + 1))) is Element of the carrier of Rseq
- ((Rseq,X) . (n + (m + 1))) is Element of the carrier of Rseq
((Rseq,X) . n) + (- ((Rseq,X) . (n + (m + 1)))) is Element of the carrier of Rseq
||.(((Rseq,X) . n) - ((Rseq,X) . (n + (m + 1)))).|| is V11() real ext-real Element of REAL
(Rseq,X) . (n + m) is Element of the carrier of Rseq
((Rseq,X) . (n + m)) + (X . ((n + m) + 1)) is Element of the carrier of Rseq
((Rseq,X) . n) - (((Rseq,X) . (n + m)) + (X . ((n + m) + 1))) is Element of the carrier of Rseq
- (((Rseq,X) . (n + m)) + (X . ((n + m) + 1))) is Element of the carrier of Rseq
((Rseq,X) . n) + (- (((Rseq,X) . (n + m)) + (X . ((n + m) + 1)))) is Element of the carrier of Rseq
||.(((Rseq,X) . n) - (((Rseq,X) . (n + m)) + (X . ((n + m) + 1)))).|| is V11() real ext-real Element of REAL
((Rseq,X) . n) - ((Rseq,X) . (n + m)) is Element of the carrier of Rseq
- ((Rseq,X) . (n + m)) is Element of the carrier of Rseq
((Rseq,X) . n) + (- ((Rseq,X) . (n + m))) is Element of the carrier of Rseq
(((Rseq,X) . n) - ((Rseq,X) . (n + m))) - (X . ((n + m) + 1)) is Element of the carrier of Rseq
- (X . ((n + m) + 1)) is Element of the carrier of Rseq
(((Rseq,X) . n) - ((Rseq,X) . (n + m))) + (- (X . ((n + m) + 1))) is Element of the carrier of Rseq
||.((((Rseq,X) . n) - ((Rseq,X) . (n + m))) - (X . ((n + m) + 1))).|| is V11() real ext-real Element of REAL
(((Rseq,X) . n) - ((Rseq,X) . (n + m))) + (- (X . ((n + m) + 1))) is Element of the carrier of Rseq
||.((((Rseq,X) . n) - ((Rseq,X) . (n + m))) + (- (X . ((n + m) + 1)))).|| is V11() real ext-real Element of REAL
||.(((Rseq,X) . n) - ((Rseq,X) . (n + m))).|| is V11() real ext-real Element of REAL
||.(- (X . ((n + m) + 1))).|| is V11() real ext-real Element of REAL
||.(((Rseq,X) . n) - ((Rseq,X) . (n + m))).|| + ||.(- (X . ((n + m) + 1))).|| is V11() real ext-real Element of REAL
||.(((Rseq,X) . n) - ((Rseq,X) . (n + m))).|| + ||.(X . ((n + m) + 1)).|| is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . (n + m)) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . (n + m))) is V11() real ext-real Element of REAL
(abs (((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . (n + m)))) + ||.(X . ((n + m) + 1)).|| is V11() real ext-real Element of REAL
- (((Partial_Sums ||.X.||) . (n + m)) - ((Partial_Sums ||.X.||) . n)) is V11() real ext-real Element of REAL
abs (- (((Partial_Sums ||.X.||) . (n + m)) - ((Partial_Sums ||.X.||) . n))) is V11() real ext-real Element of REAL
(abs (- (((Partial_Sums ||.X.||) . (n + m)) - ((Partial_Sums ||.X.||) . n)))) + ||.(X . ((n + m) + 1)).|| is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . (n + m)) - ((Partial_Sums ||.X.||) . n)) is V11() real ext-real Element of REAL
(abs (((Partial_Sums ||.X.||) . (n + m)) - ((Partial_Sums ||.X.||) . n))) + ||.(X . ((n + m) + 1)).|| is V11() real ext-real Element of REAL
k is V11() real ext-real integer set
k is V11() real ext-real integer set
k - k is V11() real ext-real integer set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . (n + 0) is Element of the carrier of Rseq
((Rseq,X) . n) - ((Rseq,X) . (n + 0)) is Element of the carrier of Rseq
- ((Rseq,X) . (n + 0)) is Element of the carrier of Rseq
((Rseq,X) . n) + (- ((Rseq,X) . (n + 0))) is Element of the carrier of Rseq
||.(((Rseq,X) . n) - ((Rseq,X) . (n + 0))).|| is V11() real ext-real Element of REAL
0. Rseq is V80(Rseq) Element of the carrier of Rseq
||.H₁(Rseq).|| is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . (n + 0) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . (n + 0)) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . n) - ((Partial_Sums ||.X.||) . (n + 0))) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(seq + m) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . ((seq + m) + 1) is Element of the carrier of Rseq
||.(X . ((seq + m) + 1)).|| is V11() real ext-real Element of REAL
m + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq + (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.X.||) . (seq + (m + 1)) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . (seq + (m + 1))) - ((Partial_Sums ||.X.||) . seq) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . (seq + (m + 1))) - ((Partial_Sums ||.X.||) . seq)) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . (seq + m) is V11() real ext-real Element of REAL
||.X.|| . ((seq + m) + 1) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . (seq + m)) + (||.X.|| . ((seq + m) + 1)) is V11() real ext-real Element of REAL
(((Partial_Sums ||.X.||) . (seq + m)) + (||.X.|| . ((seq + m) + 1))) - ((Partial_Sums ||.X.||) . seq) is V11() real ext-real Element of REAL
abs ((((Partial_Sums ||.X.||) . (seq + m)) + (||.X.|| . ((seq + m) + 1))) - ((Partial_Sums ||.X.||) . seq)) is V11() real ext-real Element of REAL
||.(X . ((seq + m) + 1)).|| + ((Partial_Sums ||.X.||) . (seq + m)) is V11() real ext-real Element of REAL
(||.(X . ((seq + m) + 1)).|| + ((Partial_Sums ||.X.||) . (seq + m))) - ((Partial_Sums ||.X.||) . seq) is V11() real ext-real Element of REAL
abs ((||.(X . ((seq + m) + 1)).|| + ((Partial_Sums ||.X.||) . (seq + m))) - ((Partial_Sums ||.X.||) . seq)) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . (seq + m)) - ((Partial_Sums ||.X.||) . seq) is V11() real ext-real Element of REAL
||.(X . ((seq + m) + 1)).|| + (((Partial_Sums ||.X.||) . (seq + m)) - ((Partial_Sums ||.X.||) . seq)) is V11() real ext-real Element of REAL
abs (||.(X . ((seq + m) + 1)).|| + (((Partial_Sums ||.X.||) . (seq + m)) - ((Partial_Sums ||.X.||) . seq))) is V11() real ext-real Element of REAL
(Rseq,X) . (seq + m) is Element of the carrier of Rseq
((Rseq,X) . (seq + m)) - ((Rseq,X) . seq) is Element of the carrier of Rseq
((Rseq,X) . (seq + m)) + (- ((Rseq,X) . seq)) is Element of the carrier of Rseq
||.(((Rseq,X) . (seq + m)) - ((Rseq,X) . seq)).|| is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . (seq + m)) - ((Partial_Sums ||.X.||) . seq)) is V11() real ext-real Element of REAL
||.(X . ((seq + m) + 1)).|| + ||.(((Rseq,X) . (seq + m)) - ((Rseq,X) . seq)).|| is V11() real ext-real Element of REAL
||.(X . ((seq + m) + 1)).|| + (abs (((Partial_Sums ||.X.||) . (seq + m)) - ((Partial_Sums ||.X.||) . seq))) is V11() real ext-real Element of REAL
(Rseq,X) . (seq + (m + 1)) is Element of the carrier of Rseq
((Rseq,X) . (seq + (m + 1))) - ((Rseq,X) . seq) is Element of the carrier of Rseq
((Rseq,X) . (seq + (m + 1))) + (- ((Rseq,X) . seq)) is Element of the carrier of Rseq
||.(((Rseq,X) . (seq + (m + 1))) - ((Rseq,X) . seq)).|| is V11() real ext-real Element of REAL
(X . ((seq + m) + 1)) + ((Rseq,X) . (seq + m)) is Element of the carrier of Rseq
((X . ((seq + m) + 1)) + ((Rseq,X) . (seq + m))) - ((Rseq,X) . seq) is Element of the carrier of Rseq
((X . ((seq + m) + 1)) + ((Rseq,X) . (seq + m))) + (- ((Rseq,X) . seq)) is Element of the carrier of Rseq
||.(((X . ((seq + m) + 1)) + ((Rseq,X) . (seq + m))) - ((Rseq,X) . seq)).|| is V11() real ext-real Element of REAL
(X . ((seq + m) + 1)) + (((Rseq,X) . (seq + m)) - ((Rseq,X) . seq)) is Element of the carrier of Rseq
||.((X . ((seq + m) + 1)) + (((Rseq,X) . (seq + m)) - ((Rseq,X) . seq))).|| is V11() real ext-real Element of REAL
k is V11() real ext-real integer set
k is V11() real ext-real integer set
k - k is V11() real ext-real integer set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . (seq + 0) is Element of the carrier of Rseq
((Rseq,X) . (seq + 0)) - ((Rseq,X) . seq) is Element of the carrier of Rseq
((Rseq,X) . (seq + 0)) + (- ((Rseq,X) . seq)) is Element of the carrier of Rseq
||.(((Rseq,X) . (seq + 0)) - ((Rseq,X) . seq)).|| is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . (seq + 0) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . (seq + 0)) - ((Partial_Sums ||.X.||) . seq) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . (seq + 0)) - ((Partial_Sums ||.X.||) . seq)) is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,n) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . n is Element of the carrier of Rseq
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,seq) is Element of the carrier of Rseq
(Rseq,X) . seq is Element of the carrier of Rseq
(Rseq,X,n) - (Rseq,X,seq) is Element of the carrier of Rseq
- (Rseq,X,seq) is Element of the carrier of Rseq
(Rseq,X,n) + (- (Rseq,X,seq)) is Element of the carrier of Rseq
||.((Rseq,X,n) - (Rseq,X,seq)).|| is V11() real ext-real Element of REAL
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Sum (||.X.||,n) is V11() real ext-real Element of REAL
Partial_Sums ||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.X.||) . n is V11() real ext-real Element of REAL
Sum (||.X.||,seq) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . seq is V11() real ext-real Element of REAL
(Sum (||.X.||,n)) - (Sum (||.X.||,seq)) is V11() real ext-real Element of REAL
abs ((Sum (||.X.||,n)) - (Sum (||.X.||,seq))) is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X,n,seq) is Element of the carrier of Rseq
(Rseq,X,n) is Element of the carrier of Rseq
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
(Rseq,X) . n is Element of the carrier of Rseq
(Rseq,X,seq) is Element of the carrier of Rseq
(Rseq,X) . seq is Element of the carrier of Rseq
(Rseq,X,n) - (Rseq,X,seq) is Element of the carrier of Rseq
- (Rseq,X,seq) is Element of the carrier of Rseq
(Rseq,X,n) + (- (Rseq,X,seq)) is Element of the carrier of Rseq
||.(Rseq,X,n,seq).|| is V11() real ext-real Element of REAL
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Sum (||.X.||,n,seq) is V11() real ext-real Element of REAL
Sum (||.X.||,n) is V11() real ext-real Element of REAL
Partial_Sums ||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Partial_Sums ||.X.||) . n is V11() real ext-real Element of REAL
Sum (||.X.||,seq) is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . seq is V11() real ext-real Element of REAL
(Sum (||.X.||,n)) - (Sum (||.X.||,seq)) is V11() real ext-real Element of REAL
abs (Sum (||.X.||,n,seq)) is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like V144() UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq is V11() real ext-real Element of REAL
seq / 2 is V11() real ext-real Element of REAL
Partial_Sums ||.X.|| is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.X.||) . n is V11() real ext-real Element of REAL
(Rseq,X) is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . m1 is Element of the carrier of Rseq
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . k is Element of the carrier of Rseq
((Rseq,X) . m1) - ((Rseq,X) . k) is Element of the carrier of Rseq
- ((Rseq,X) . k) is Element of the carrier of Rseq
((Rseq,X) . m1) + (- ((Rseq,X) . k)) is Element of the carrier of Rseq
||.(((Rseq,X) . m1) - ((Rseq,X) . k)).|| is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . m1 is V11() real ext-real Element of REAL
(Partial_Sums ||.X.||) . k is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . m1) - ((Partial_Sums ||.X.||) . k) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . m1) - ((Partial_Sums ||.X.||) . k)) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.X.||) . k is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . k) - ((Partial_Sums ||.X.||) . k) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . k) - ((Partial_Sums ||.X.||) . k)) is V11() real ext-real Element of REAL
((Partial_Sums ||.X.||) . m1) - ((Partial_Sums ||.X.||) . k) is V11() real ext-real Element of REAL
abs (((Partial_Sums ||.X.||) . m1) - ((Partial_Sums ||.X.||) . k)) is V11() real ext-real Element of REAL
(seq / 2) + (seq / 2) is V11() real ext-real Element of REAL
(abs (((Partial_Sums ||.X.||) . m1) - ((Partial_Sums ||.X.||) . k))) + (abs (((Partial_Sums ||.X.||) . k) - ((Partial_Sums ||.X.||) . k))) is V11() real ext-real Element of REAL
(((Partial_Sums ||.X.||) . m1) - ((Partial_Sums ||.X.||) . k)) - (((Partial_Sums ||.X.||) . k) - ((Partial_Sums ||.X.||) . k)) is V11() real ext-real Element of REAL
abs ((((Partial_Sums ||.X.||) . m1) - ((Partial_Sums ||.X.||) . k)) - (((Partial_Sums ||.X.||) . k) - ((Partial_Sums ||.X.||) . k))) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Rseq,X) . k is Element of the carrier of Rseq
(Rseq,X) . m1 is Element of the carrier of Rseq
((Rseq,X) . k) - ((Rseq,X) . m1) is Element of the carrier of Rseq
- ((Rseq,X) . m1) is Element of the carrier of Rseq
((Rseq,X) . k) + (- ((Rseq,X) . m1)) is Element of the carrier of Rseq
||.(((Rseq,X) . k) - ((Rseq,X) . m1)).|| is V11() real ext-real Element of REAL
Rseq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of Rseq is V1() set
K7(NAT, the carrier of Rseq) is set
K6(K7(NAT, the carrier of Rseq)) is set
X is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
seq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
k is V1() V16() V19( NAT ) V20( the carrier of Rseq) V21() V26( NAT ) V30( NAT , the carrier of Rseq) Element of K6(K7(NAT, the carrier of Rseq))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
K68(n,k) is set
K68(k,k) is set
n . k is Element of the carrier of Rseq
X . k is Element of the carrier of Rseq
seq . k is V11() real ext-real Element of REAL
(seq . k) * (X . k) is Element of the carrier of Rseq
k . k is Element of the carrier of Rseq
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + n is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq + n),Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,n,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,Rseq) + (X,n,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() 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 integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
K68((X,(seq + n),Rseq),k) is set
K68(((X,seq,Rseq) + (X,n,Rseq)),k) is set
(X,(seq + n),Rseq) . k is Element of the carrier of X
(seq + n) . k is Element of the carrier of X
Rseq . k is V11() real ext-real Element of REAL
(Rseq . k) * ((seq + n) . k) is Element of the carrier of X
seq . k is Element of the carrier of X
n . k is Element of the carrier of X
(seq . k) + (n . k) is Element of the carrier of X
(Rseq . k) * ((seq . k) + (n . k)) is Element of the carrier of X
(Rseq . k) * (seq . k) is Element of the carrier of X
(Rseq . k) * (n . k) is Element of the carrier of X
((Rseq . k) * (seq . k)) + ((Rseq . k) * (n . k)) is Element of the carrier of X
(X,seq,Rseq) . k is Element of the carrier of X
((X,seq,Rseq) . k) + ((Rseq . k) * (n . k)) is Element of the carrier of X
(X,n,Rseq) . k is Element of the carrier of X
((X,seq,Rseq) . k) + ((X,n,Rseq) . k) is Element of the carrier of X
((X,seq,Rseq) + (X,n,Rseq)) . k is Element of the carrier of X
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
X is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Rseq + X is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of seq is V1() set
K7(NAT, the carrier of seq) is set
K6(K7(NAT, the carrier of seq)) is set
n is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n,(Rseq + X)) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n,Rseq) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n,X) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n,Rseq) + (seq,n,X) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
K68((seq,n,(Rseq + X)),k) is set
K68(((seq,n,Rseq) + (seq,n,X)),k) is set
(seq,n,(Rseq + X)) . k is Element of the carrier of seq
n . k is Element of the carrier of seq
(Rseq + X) . k is V11() real ext-real Element of REAL
((Rseq + X) . k) * (n . k) is Element of the carrier of seq
Rseq . k is V11() real ext-real Element of REAL
X . k is V11() real ext-real Element of REAL
(Rseq . k) + (X . k) is V11() real ext-real Element of REAL
((Rseq . k) + (X . k)) * (n . k) is Element of the carrier of seq
(Rseq . k) * (n . k) is Element of the carrier of seq
(X . k) * (n . k) is Element of the carrier of seq
((Rseq . k) * (n . k)) + ((X . k) * (n . k)) is Element of the carrier of seq
(seq,n,Rseq) . k is Element of the carrier of seq
((seq,n,Rseq) . k) + ((X . k) * (n . k)) is Element of the carrier of seq
(seq,n,X) . k is Element of the carrier of seq
((seq,n,Rseq) . k) + ((seq,n,X) . k) is Element of the carrier of seq
((seq,n,Rseq) + (seq,n,X)) . k is Element of the carrier of seq
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
X is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Rseq (#) X is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of seq is V1() set
K7(NAT, the carrier of seq) is set
K6(K7(NAT, the carrier of seq)) is set
n is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n,(Rseq (#) X)) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n,X) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,(seq,n,X),Rseq) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
K68((seq,n,(Rseq (#) X)),k) is set
K68((seq,(seq,n,X),Rseq),k) is set
(seq,n,(Rseq (#) X)) . k is Element of the carrier of seq
n . k is Element of the carrier of seq
(Rseq (#) X) . k is V11() real ext-real Element of REAL
((Rseq (#) X) . k) * (n . k) is Element of the carrier of seq
Rseq . k is V11() real ext-real Element of REAL
X . k is V11() real ext-real Element of REAL
(Rseq . k) * (X . k) is V11() real ext-real Element of REAL
((Rseq . k) * (X . k)) * (n . k) is Element of the carrier of seq
(X . k) * (n . k) is Element of the carrier of seq
(Rseq . k) * ((X . k) * (n . k)) is Element of the carrier of seq
(seq,n,X) . k is Element of the carrier of seq
(Rseq . k) * ((seq,n,X) . k) is Element of the carrier of seq
(seq,(seq,n,X),Rseq) . k is Element of the carrier of seq
Rseq is V11() real ext-real Element of REAL
X is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Rseq (#) X is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of seq is V1() set
K7(NAT, the carrier of seq) is set
K6(K7(NAT, the carrier of seq)) is set
n is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n,(Rseq (#) X)) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
(seq,n,X) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
Rseq * (seq,n,X) is V1() V16() V19( NAT ) V20( the carrier of seq) V21() V26( NAT ) V30( NAT , the carrier of seq) Element of K6(K7(NAT, the carrier of seq))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
K68((seq,n,(Rseq (#) X)),k) is set
K68((Rseq * (seq,n,X)),k) is set
(seq,n,(Rseq (#) X)) . k is Element of the carrier of seq
n . k is Element of the carrier of seq
(Rseq (#) X) . k is V11() real ext-real Element of REAL
((Rseq (#) X) . k) * (n . k) is Element of the carrier of seq
X . k is V11() real ext-real Element of REAL
Rseq * (X . k) is V11() real ext-real Element of REAL
(Rseq * (X . k)) * (n . k) is Element of the carrier of seq
(X . k) * (n . k) is Element of the carrier of seq
Rseq * ((X . k) * (n . k)) is Element of the carrier of seq
(seq,n,X) . k is Element of the carrier of seq
Rseq * ((seq,n,X) . k) is Element of the carrier of seq
(Rseq * (seq,n,X)) . k is Element of the carrier of seq
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real non positive integer set
(- 1) (#) Rseq is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(- seq),Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,(- Rseq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
K68((X,(- seq),Rseq),n) is set
K68((X,seq,(- Rseq)),n) is set
(X,(- seq),Rseq) . n is Element of the carrier of X
(- seq) . n is Element of the carrier of X
Rseq . n is V11() real ext-real Element of REAL
(Rseq . n) * ((- seq) . n) is Element of the carrier of X
seq . n is Element of the carrier of X
- (seq . n) is Element of the carrier of X
(Rseq . n) * (- (seq . n)) is Element of the carrier of X
- (Rseq . n) is V11() real ext-real Element of REAL
(- (Rseq . n)) * (seq . n) is Element of the carrier of X
(- Rseq) . n is V11() real ext-real Element of REAL
((- Rseq) . n) * (seq . n) is Element of the carrier of X
(X,seq,(- Rseq)) . n is Element of the carrier of X
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is V11() real ext-real set
k is Element of the carrier of X
k is V11() real ext-real Element of REAL
k * k is Element of the carrier of X
m is V11() real ext-real set
n is V11() real ext-real Element of REAL
||.k.|| is V11() real ext-real Element of REAL
n + ||.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 integer V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
m2 is V11() real ext-real Element of REAL
m2 / (n + ||.k.||) is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m1 + m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . n is V11() real ext-real Element of REAL
(Rseq . n) - k is V11() real ext-real Element of REAL
abs ((Rseq . n) - k) is V11() real ext-real Element of REAL
||.k.|| * (abs ((Rseq . n) - k)) is V11() real ext-real Element of REAL
||.k.|| * (m2 / (n + ||.k.||)) is V11() real ext-real Element of REAL
abs (Rseq . n) is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
(seq . n) - k is Element of the carrier of X
- k is Element of the carrier of X
(seq . n) + (- k) is Element of the carrier of X
||.((seq . n) - k).|| is V11() real ext-real Element of REAL
n * (m2 / (n + ||.k.||)) is V11() real ext-real Element of REAL
(abs (Rseq . n)) * ||.((seq . n) - k).|| is V11() real ext-real Element of REAL
(n * (m2 / (n + ||.k.||))) + (||.k.|| * (m2 / (n + ||.k.||))) is V11() real ext-real Element of REAL
((abs (Rseq . n)) * ||.((seq . n) - k).||) + (||.k.|| * (abs ((Rseq . n) - k))) is V11() real ext-real Element of REAL
n * m2 is V11() real ext-real Element of REAL
(n * m2) / (n + ||.k.||) is V11() real ext-real Element of REAL
((n * m2) / (n + ||.k.||)) + (||.k.|| * (m2 / (n + ||.k.||))) is V11() real ext-real Element of REAL
||.k.|| * m2 is V11() real ext-real Element of REAL
(||.k.|| * m2) / (n + ||.k.||) is V11() real ext-real Element of REAL
((n * m2) / (n + ||.k.||)) + ((||.k.|| * m2) / (n + ||.k.||)) is V11() real ext-real Element of REAL
(n * m2) + (||.k.|| * m2) is V11() real ext-real Element of REAL
((n * m2) + (||.k.|| * m2)) / (n + ||.k.||) is V11() real ext-real Element of REAL
(n + ||.k.||) * m2 is V11() real ext-real Element of REAL
((n + ||.k.||) * m2) / (n + ||.k.||) is V11() real ext-real Element of REAL
(X,seq,Rseq) . n is Element of the carrier of X
((X,seq,Rseq) . n) - (k * k) is Element of the carrier of X
- (k * k) is Element of the carrier of X
((X,seq,Rseq) . n) + (- (k * k)) is Element of the carrier of X
||.(((X,seq,Rseq) . n) - (k * k)).|| is V11() real ext-real Element of REAL
(Rseq . n) * (seq . n) is Element of the carrier of X
((Rseq . n) * (seq . n)) - (k * k) is Element of the carrier of X
((Rseq . n) * (seq . n)) + (- (k * k)) is Element of the carrier of X
||.(((Rseq . n) * (seq . n)) - (k * k)).|| is V11() real ext-real Element of REAL
0. X is V80(X) Element of the carrier of X
(((Rseq . n) * (seq . n)) - (k * k)) + H₁(X) is Element of the carrier of X
||.((((Rseq . n) * (seq . n)) - (k * k)) + H₁(X)).|| is V11() real ext-real Element of REAL
(Rseq . n) * k is Element of the carrier of X
((Rseq . n) * k) - ((Rseq . n) * k) is Element of the carrier of X
- ((Rseq . n) * k) is Element of the carrier of X
((Rseq . n) * k) + (- ((Rseq . n) * k)) is Element of the carrier of X
(((Rseq . n) * (seq . n)) - (k * k)) + (((Rseq . n) * k) - ((Rseq . n) * k)) is Element of the carrier of X
||.((((Rseq . n) * (seq . n)) - (k * k)) + (((Rseq . n) * k) - ((Rseq . n) * k))).|| is V11() real ext-real Element of REAL
(k * k) - (((Rseq . n) * k) - ((Rseq . n) * k)) is Element of the carrier of X
- (((Rseq . n) * k) - ((Rseq . n) * k)) is Element of the carrier of X
(k * k) + (- (((Rseq . n) * k) - ((Rseq . n) * k))) is Element of the carrier of X
((Rseq . n) * (seq . n)) - ((k * k) - (((Rseq . n) * k) - ((Rseq . n) * k))) is Element of the carrier of X
- ((k * k) - (((Rseq . n) * k) - ((Rseq . n) * k))) is Element of the carrier of X
((Rseq . n) * (seq . n)) + (- ((k * k) - (((Rseq . n) * k) - ((Rseq . n) * k)))) is Element of the carrier of X
||.(((Rseq . n) * (seq . n)) - ((k * k) - (((Rseq . n) * k) - ((Rseq . n) * k)))).|| is V11() real ext-real Element of REAL
(k * k) - ((Rseq . n) * k) is Element of the carrier of X
(k * k) + (- ((Rseq . n) * k)) is Element of the carrier of X
((Rseq . n) * k) + ((k * k) - ((Rseq . n) * k)) is Element of the carrier of X
((Rseq . n) * (seq . n)) - (((Rseq . n) * k) + ((k * k) - ((Rseq . n) * k))) is Element of the carrier of X
- (((Rseq . n) * k) + ((k * k) - ((Rseq . n) * k))) is Element of the carrier of X
((Rseq . n) * (seq . n)) + (- (((Rseq . n) * k) + ((k * k) - ((Rseq . n) * k)))) is Element of the carrier of X
||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * k) + ((k * k) - ((Rseq . n) * k)))).|| is V11() real ext-real Element of REAL
((Rseq . n) * (seq . n)) - ((Rseq . n) * k) is Element of the carrier of X
((Rseq . n) * (seq . n)) + (- ((Rseq . n) * k)) is Element of the carrier of X
(((Rseq . n) * (seq . n)) - ((Rseq . n) * k)) - ((k * k) - ((Rseq . n) * k)) is Element of the carrier of X
- ((k * k) - ((Rseq . n) * k)) is Element of the carrier of X
(((Rseq . n) * (seq . n)) - ((Rseq . n) * k)) + (- ((k * k) - ((Rseq . n) * k))) is Element of the carrier of X
||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * k)) - ((k * k) - ((Rseq . n) * k))).|| is V11() real ext-real Element of REAL
((Rseq . n) * k) - (k * k) is Element of the carrier of X
((Rseq . n) * k) + (- (k * k)) is Element of the carrier of X
(((Rseq . n) * (seq . n)) - ((Rseq . n) * k)) + (((Rseq . n) * k) - (k * k)) is Element of the carrier of X
||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * k)) + (((Rseq . n) * k) - (k * k))).|| is V11() real ext-real Element of REAL
||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * k)).|| is V11() real ext-real Element of REAL
||.(((Rseq . n) * k) - (k * k)).|| is V11() real ext-real Element of REAL
||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * k)).|| + ||.(((Rseq . n) * k) - (k * k)).|| is V11() real ext-real Element of REAL
(Rseq . n) * ((seq . n) - k) is Element of the carrier of X
||.((Rseq . n) * ((seq . n) - k)).|| is V11() real ext-real Element of REAL
||.((Rseq . n) * ((seq . n) - k)).|| + ||.(((Rseq . n) * k) - (k * k)).|| is V11() real ext-real Element of REAL
((Rseq . n) - k) * k is Element of the carrier of X
||.(((Rseq . n) - k) * k).|| is V11() real ext-real Element of REAL
||.((Rseq . n) * ((seq . n) - k)).|| + ||.(((Rseq . n) - k) * k).|| is V11() real ext-real Element of REAL
((abs (Rseq . n)) * ||.((seq . n) - k).||) + ||.(((Rseq . n) - k) * k).|| is V11() real ext-real Element of REAL
m1 is Element of the carrier of X
((X,seq,Rseq) . n) - m1 is Element of the carrier of X
- m1 is Element of the carrier of X
((X,seq,Rseq) . n) + (- m1) is Element of the carrier of X
||.(((X,seq,Rseq) . n) - m1).|| is V11() real ext-real Element of REAL
m1 is Element of the carrier of X
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is V11() real ext-real set
k is V11() real ext-real Element of REAL
n * k is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . m2 is V11() real ext-real Element of REAL
abs (Rseq . m2) is V11() real ext-real Element of REAL
seq . m2 is Element of the carrier of X
||.(seq . m2).|| is V11() real ext-real Element of REAL
(abs (Rseq . m2)) * ||.(seq . m2).|| is V11() real ext-real Element of REAL
(abs (Rseq . m2)) * k is V11() real ext-real Element of REAL
(X,seq,Rseq) . m2 is Element of the carrier of X
||.((X,seq,Rseq) . m2).|| is V11() real ext-real Element of REAL
(Rseq . m2) * (seq . m2) is Element of the carrier of X
||.((Rseq . m2) * (seq . m2)).|| is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,seq,Rseq) . m2 is Element of the carrier of X
||.((X,seq,Rseq) . m2).|| is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim Rseq is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
lim (X,seq,Rseq) is Element of the carrier of X
lim seq is Element of the carrier of X
(lim Rseq) * (lim seq) is Element of the carrier of X
n is V11() real ext-real set
k is V11() real ext-real Element of REAL
||.(lim seq).|| is V11() real ext-real Element of REAL
k + ||.(lim seq).|| 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 integer V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
k is V11() real ext-real Element of REAL
k / (k + ||.(lim seq).||) is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m1 + m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . n is V11() real ext-real Element of REAL
(Rseq . n) - (lim Rseq) is V11() real ext-real Element of REAL
abs ((Rseq . n) - (lim Rseq)) is V11() real ext-real Element of REAL
||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq))) is V11() real ext-real Element of REAL
||.(lim seq).|| * (k / (k + ||.(lim seq).||)) is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
(seq . n) - (lim seq) is Element of the carrier of X
- (lim seq) is Element of the carrier of X
(seq . n) + (- (lim seq)) is Element of the carrier of X
||.((seq . n) - (lim seq)).|| is V11() real ext-real Element of REAL
dist ((seq . n),(lim seq)) is V11() real ext-real Element of REAL
abs (Rseq . n) is V11() real ext-real Element of REAL
k * (k / (k + ||.(lim seq).||)) is V11() real ext-real Element of REAL
(abs (Rseq . n)) * ||.((seq . n) - (lim seq)).|| is V11() real ext-real Element of REAL
(k * (k / (k + ||.(lim seq).||))) + (||.(lim seq).|| * (k / (k + ||.(lim seq).||))) is V11() real ext-real Element of REAL
((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) is V11() real ext-real Element of REAL
k * k is V11() real ext-real Element of REAL
(k * k) / (k + ||.(lim seq).||) is V11() real ext-real Element of REAL
((k * k) / (k + ||.(lim seq).||)) + (||.(lim seq).|| * (k / (k + ||.(lim seq).||))) is V11() real ext-real Element of REAL
||.(lim seq).|| * k is V11() real ext-real Element of REAL
(||.(lim seq).|| * k) / (k + ||.(lim seq).||) is V11() real ext-real Element of REAL
((k * k) / (k + ||.(lim seq).||)) + ((||.(lim seq).|| * k) / (k + ||.(lim seq).||)) is V11() real ext-real Element of REAL
(k * k) + (||.(lim seq).|| * k) is V11() real ext-real Element of REAL
((k * k) + (||.(lim seq).|| * k)) / (k + ||.(lim seq).||) is V11() real ext-real Element of REAL
(k + ||.(lim seq).||) * k is V11() real ext-real Element of REAL
((k + ||.(lim seq).||) * k) / (k + ||.(lim seq).||) is V11() real ext-real Element of REAL
(X,seq,Rseq) . n is Element of the carrier of X
((X,seq,Rseq) . n) - ((lim Rseq) * (lim seq)) is Element of the carrier of X
- ((lim Rseq) * (lim seq)) is Element of the carrier of X
((X,seq,Rseq) . n) + (- ((lim Rseq) * (lim seq))) is Element of the carrier of X
||.(((X,seq,Rseq) . n) - ((lim Rseq) * (lim seq))).|| is V11() real ext-real Element of REAL
(Rseq . n) * (seq . n) is Element of the carrier of X
((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq)) is Element of the carrier of X
((Rseq . n) * (seq . n)) + (- ((lim Rseq) * (lim seq))) is Element of the carrier of X
||.(((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))).|| is V11() real ext-real Element of REAL
0. X is V80(X) Element of the carrier of X
(((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + H₁(X) is Element of the carrier of X
||.((((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + H₁(X)).|| is V11() real ext-real Element of REAL
(Rseq . n) * (lim seq) is Element of the carrier of X
((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq)) is Element of the carrier of X
- ((Rseq . n) * (lim seq)) is Element of the carrier of X
((Rseq . n) * (lim seq)) + (- ((Rseq . n) * (lim seq))) is Element of the carrier of X
(((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq))) is Element of the carrier of X
||.((((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq)))).|| is V11() real ext-real Element of REAL
((lim Rseq) * (lim seq)) - (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq))) is Element of the carrier of X
- (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq))) is Element of the carrier of X
((lim Rseq) * (lim seq)) + (- (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq)))) is Element of the carrier of X
((Rseq . n) * (seq . n)) - (((lim Rseq) * (lim seq)) - (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq)))) is Element of the carrier of X
- (((lim Rseq) * (lim seq)) - (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq)))) is Element of the carrier of X
((Rseq . n) * (seq . n)) + (- (((lim Rseq) * (lim seq)) - (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq))))) is Element of the carrier of X
||.(((Rseq . n) * (seq . n)) - (((lim Rseq) * (lim seq)) - (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq))))).|| is V11() real ext-real Element of REAL
((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq)) is Element of the carrier of X
((lim Rseq) * (lim seq)) + (- ((Rseq . n) * (lim seq))) is Element of the carrier of X
((Rseq . n) * (lim seq)) + (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq))) is Element of the carrier of X
((Rseq . n) * (seq . n)) - (((Rseq . n) * (lim seq)) + (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq)))) is Element of the carrier of X
- (((Rseq . n) * (lim seq)) + (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq)))) is Element of the carrier of X
((Rseq . n) * (seq . n)) + (- (((Rseq . n) * (lim seq)) + (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq))))) is Element of the carrier of X
||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * (lim seq)) + (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq))))).|| is V11() real ext-real Element of REAL
((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq)) is Element of the carrier of X
((Rseq . n) * (seq . n)) + (- ((Rseq . n) * (lim seq))) is Element of the carrier of X
(((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) - (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq))) is Element of the carrier of X
- (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq))) is Element of the carrier of X
(((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) + (- (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq)))) is Element of the carrier of X
||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) - (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq)))).|| is V11() real ext-real Element of REAL
((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq)) is Element of the carrier of X
((Rseq . n) * (lim seq)) + (- ((lim Rseq) * (lim seq))) is Element of the carrier of X
(((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))) is Element of the carrier of X
||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq)))).|| is V11() real ext-real Element of REAL
||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))).|| is V11() real ext-real Element of REAL
||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).|| is V11() real ext-real Element of REAL
||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))).|| + ||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).|| is V11() real ext-real Element of REAL
(Rseq . n) * ((seq . n) - (lim seq)) is Element of the carrier of X
||.((Rseq . n) * ((seq . n) - (lim seq))).|| is V11() real ext-real Element of REAL
||.((Rseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).|| is V11() real ext-real Element of REAL
((Rseq . n) - (lim Rseq)) * (lim seq) is Element of the carrier of X
||.(((Rseq . n) - (lim Rseq)) * (lim seq)).|| is V11() real ext-real Element of REAL
||.((Rseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Rseq . n) - (lim Rseq)) * (lim seq)).|| is V11() real ext-real Element of REAL
((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + ||.(((Rseq . n) - (lim Rseq)) * (lim seq)).|| is V11() real ext-real Element of REAL
dist (((X,seq,Rseq) . n),((lim Rseq) * (lim seq))) is V11() real ext-real Element of REAL
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like V144() UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . k is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . m1 is V11() real ext-real Element of REAL
(Rseq . m1) - (Rseq . k) is V11() real ext-real Element of REAL
abs ((Rseq . m1) - (Rseq . k)) is V11() real ext-real Element of REAL
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Rseq ^\ 1 is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Rseq
Rseq - (Rseq ^\ 1) is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- (Rseq ^\ 1) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive integer set
(- 1) (#) (Rseq ^\ 1) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
Rseq + (- (Rseq ^\ 1)) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq),(Rseq - (Rseq ^\ 1))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq,Rseq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq),Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . 0 is Element of the carrier of X
(X,(X,seq),(Rseq - (Rseq ^\ 1))) . 0 is Element of the carrier of X
(X,seq) . 0 is Element of the carrier of X
(Rseq - (Rseq ^\ 1)) . 0 is V11() real ext-real Element of REAL
((Rseq - (Rseq ^\ 1)) . 0) * ((X,seq) . 0) is Element of the carrier of X
seq . 0 is Element of the carrier of X
- (Rseq ^\ 1) is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Rseq + (- (Rseq ^\ 1)) is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(Rseq + (- (Rseq ^\ 1))) . 0 is V11() real ext-real Element of REAL
((Rseq + (- (Rseq ^\ 1))) . 0) * (seq . 0) is Element of the carrier of X
Rseq . 0 is V11() real ext-real Element of REAL
(- (Rseq ^\ 1)) . 0 is V11() real ext-real Element of REAL
(Rseq . 0) + ((- (Rseq ^\ 1)) . 0) is V11() real ext-real Element of REAL
((Rseq . 0) + ((- (Rseq ^\ 1)) . 0)) * (seq . 0) is Element of the carrier of X
(Rseq ^\ 1) . 0 is V11() real ext-real Element of REAL
- ((Rseq ^\ 1) . 0) is V11() real ext-real Element of REAL
(Rseq . 0) + (- ((Rseq ^\ 1) . 0)) is V11() real ext-real Element of REAL
((Rseq . 0) + (- ((Rseq ^\ 1) . 0))) * (seq . 0) is Element of the carrier of X
(Rseq . 0) - ((Rseq ^\ 1) . 0) is V11() real ext-real Element of REAL
((Rseq . 0) - ((Rseq ^\ 1) . 0)) * (seq . 0) is Element of the carrier of X
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Rseq . (0 + 1) is V11() real ext-real Element of REAL
(Rseq . 0) - (Rseq . (0 + 1)) is V11() real ext-real Element of REAL
((Rseq . 0) - (Rseq . (0 + 1))) * (seq . 0) is Element of the carrier of X
(Rseq . 0) * (seq . 0) is Element of the carrier of X
Rseq . 1 is V11() real ext-real Element of REAL
(Rseq . 1) * (seq . 0) is Element of the carrier of X
((Rseq . 0) * (seq . 0)) - ((Rseq . 1) * (seq . 0)) is Element of the carrier of X
- ((Rseq . 1) * (seq . 0)) is Element of the carrier of X
((Rseq . 0) * (seq . 0)) + (- ((Rseq . 1) * (seq . 0))) is Element of the carrier of X
(X,(X,seq),Rseq) . (0 + 1) is Element of the carrier of X
(X,seq) . (0 + 1) is Element of the carrier of X
(Rseq . (0 + 1)) * ((X,seq) . (0 + 1)) is Element of the carrier of X
seq . (0 + 1) is Element of the carrier of X
((X,seq) . 0) + (seq . (0 + 1)) is Element of the carrier of X
(Rseq . (0 + 1)) * (((X,seq) . 0) + (seq . (0 + 1))) is Element of the carrier of X
seq . 1 is Element of the carrier of X
(seq . 0) + (seq . 1) is Element of the carrier of X
(Rseq . 1) * ((seq . 0) + (seq . 1)) is Element of the carrier of X
(Rseq . 1) * (seq . 1) is Element of the carrier of X
((Rseq . 1) * (seq . 0)) + ((Rseq . 1) * (seq . 1)) is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n is Element of the carrier of X
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,(X,seq,Rseq)) . (n + 1) is Element of the carrier of X
(X,(X,seq),Rseq) . (n + 1) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
- ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) + (- ((X,(X,seq),Rseq) . (n + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + (- ((X,(X,seq),Rseq) . (n + 1))) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) - (((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1))) is Element of the carrier of X
- (((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1))) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) + (- (((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1)))) is Element of the carrier of X
0. X is V80(X) Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) - H₁(X) is Element of the carrier of X
- (0. X) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) + (- (0. X)) is Element of the carrier of X
(n + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,(X,seq,Rseq)) . ((n + 1) + 1) is Element of the carrier of X
(X,seq,Rseq) . ((n + 1) + 1) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) + ((X,seq,Rseq) . ((n + 1) + 1)) is Element of the carrier of X
(((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + ((X,(X,seq),Rseq) . (n + 1))) + ((X,seq,Rseq) . ((n + 1) + 1)) is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + ((X,seq,Rseq) . ((n + 1) + 1)) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((X,(X,seq),Rseq) . (n + 1)) + ((X,seq,Rseq) . ((n + 1) + 1))) is Element of the carrier of X
(X,seq) . (n + 1) is Element of the carrier of X
Rseq . (n + 1) is V11() real ext-real Element of REAL
(Rseq . (n + 1)) * ((X,seq) . (n + 1)) is Element of the carrier of X
((Rseq . (n + 1)) * ((X,seq) . (n + 1))) + ((X,seq,Rseq) . ((n + 1) + 1)) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((Rseq . (n + 1)) * ((X,seq) . (n + 1))) + ((X,seq,Rseq) . ((n + 1) + 1))) is Element of the carrier of X
Rseq . ((n + 1) + 1) is V11() real ext-real Element of REAL
(Rseq . (n + 1)) - (Rseq . ((n + 1) + 1)) is V11() real ext-real Element of REAL
((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) + (Rseq . ((n + 1) + 1)) is V11() real ext-real Element of REAL
(((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) + (Rseq . ((n + 1) + 1))) * ((X,seq) . (n + 1)) is Element of the carrier of X
seq . ((n + 1) + 1) is Element of the carrier of X
(Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)) is Element of the carrier of X
((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) + (Rseq . ((n + 1) + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) + (Rseq . ((n + 1) + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) * ((X,seq) . (n + 1)) is Element of the carrier of X
(Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)) is Element of the carrier of X
(((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) is Element of the carrier of X
((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
(Rseq ^\ 1) . (n + 1) is V11() real ext-real Element of REAL
(Rseq . (n + 1)) - ((Rseq ^\ 1) . (n + 1)) is V11() real ext-real Element of REAL
((Rseq . (n + 1)) - ((Rseq ^\ 1) . (n + 1))) * ((X,seq) . (n + 1)) is Element of the carrier of X
(((Rseq . (n + 1)) - ((Rseq ^\ 1) . (n + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) is Element of the carrier of X
((((Rseq . (n + 1)) - ((Rseq ^\ 1) . (n + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((((Rseq . (n + 1)) - ((Rseq ^\ 1) . (n + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
- ((Rseq ^\ 1) . (n + 1)) is V11() real ext-real Element of REAL
(Rseq . (n + 1)) + (- ((Rseq ^\ 1) . (n + 1))) is V11() real ext-real Element of REAL
((Rseq . (n + 1)) + (- ((Rseq ^\ 1) . (n + 1)))) * ((X,seq) . (n + 1)) is Element of the carrier of X
(((Rseq . (n + 1)) + (- ((Rseq ^\ 1) . (n + 1)))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) is Element of the carrier of X
((((Rseq . (n + 1)) + (- ((Rseq ^\ 1) . (n + 1)))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((((Rseq . (n + 1)) + (- ((Rseq ^\ 1) . (n + 1)))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
(- (Rseq ^\ 1)) . (n + 1) is V11() real ext-real Element of REAL
(Rseq . (n + 1)) + ((- (Rseq ^\ 1)) . (n + 1)) is V11() real ext-real Element of REAL
((Rseq . (n + 1)) + ((- (Rseq ^\ 1)) . (n + 1))) * ((X,seq) . (n + 1)) is Element of the carrier of X
(((Rseq . (n + 1)) + ((- (Rseq ^\ 1)) . (n + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) is Element of the carrier of X
((((Rseq . (n + 1)) + ((- (Rseq ^\ 1)) . (n + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((((Rseq . (n + 1)) + ((- (Rseq ^\ 1)) . (n + 1))) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
(Rseq - (Rseq ^\ 1)) . (n + 1) is V11() real ext-real Element of REAL
((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((X,seq) . (n + 1)) is Element of the carrier of X
(((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) is Element of the carrier of X
((((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the carrier of X
(((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((X,seq) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + ((((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((X,seq) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((X,seq) . (n + 1))) is Element of the carrier of X
(((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + (((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((X,seq) . (n + 1)))) + (((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
(X,(X,seq),(Rseq - (Rseq ^\ 1))) . (n + 1) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + ((X,(X,seq),(Rseq - (Rseq ^\ 1))) . (n + 1)) is Element of the carrier of X
(((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + ((X,(X,seq),(Rseq - (Rseq ^\ 1))) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
(X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . (n + 1) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . (n + 1)) + (((Rseq . ((n + 1) + 1)) * ((X,seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the carrier of X
((X,seq) . (n + 1)) + (seq . ((n + 1) + 1)) is Element of the carrier of X
(Rseq . ((n + 1) + 1)) * (((X,seq) . (n + 1)) + (seq . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . (n + 1)) + ((Rseq . ((n + 1) + 1)) * (((X,seq) . (n + 1)) + (seq . ((n + 1) + 1)))) is Element of the carrier of X
(X,seq) . ((n + 1) + 1) is Element of the carrier of X
(Rseq . ((n + 1) + 1)) * ((X,seq) . ((n + 1) + 1)) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . (n + 1)) + ((Rseq . ((n + 1) + 1)) * ((X,seq) . ((n + 1) + 1))) is Element of the carrier of X
(X,(X,seq),Rseq) . ((n + 1) + 1) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . (n + 1)) + ((X,(X,seq),Rseq) . ((n + 1) + 1)) is Element of the carrier of X
((X,(X,seq,Rseq)) . ((n + 1) + 1)) - ((X,(X,seq),Rseq) . ((n + 1) + 1)) is Element of the carrier of X
- ((X,(X,seq),Rseq) . ((n + 1) + 1)) is Element of the carrier of X
((X,(X,seq,Rseq)) . ((n + 1) + 1)) + (- ((X,(X,seq),Rseq) . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,seq),Rseq) . ((n + 1) + 1)) - ((X,(X,seq),Rseq) . ((n + 1) + 1)) is Element of the carrier of X
((X,(X,seq),Rseq) . ((n + 1) + 1)) + (- ((X,(X,seq),Rseq) . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . (n + 1)) + (((X,(X,seq),Rseq) . ((n + 1) + 1)) - ((X,(X,seq),Rseq) . ((n + 1) + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . (n + 1)) + H₁(X) is Element of the carrier of X
(X,(X,seq,Rseq)) . (0 + 1) is Element of the carrier of X
(X,(X,seq,Rseq)) . 0 is Element of the carrier of X
(X,seq,Rseq) . (0 + 1) is Element of the carrier of X
((X,(X,seq,Rseq)) . 0) + ((X,seq,Rseq) . (0 + 1)) is Element of the carrier of X
(X,seq,Rseq) . 0 is Element of the carrier of X
(X,seq,Rseq) . 1 is Element of the carrier of X
((X,seq,Rseq) . 0) + ((X,seq,Rseq) . 1) is Element of the carrier of X
((Rseq . 0) * (seq . 0)) + ((X,seq,Rseq) . 1) is Element of the carrier of X
((Rseq . 0) * (seq . 0)) + ((Rseq . 1) * (seq . 1)) is Element of the carrier of X
((Rseq . 0) * (seq . 0)) + H₁(X) is Element of the carrier of X
(((Rseq . 0) * (seq . 0)) + H₁(X)) + ((Rseq . 1) * (seq . 1)) is Element of the carrier of X
((Rseq . 1) * (seq . 0)) - ((Rseq . 1) * (seq . 0)) is Element of the carrier of X
((Rseq . 1) * (seq . 0)) + (- ((Rseq . 1) * (seq . 0))) is Element of the carrier of X
((Rseq . 0) * (seq . 0)) + (((Rseq . 1) * (seq . 0)) - ((Rseq . 1) * (seq . 0))) is Element of the carrier of X
(((Rseq . 0) * (seq . 0)) + (((Rseq . 1) * (seq . 0)) - ((Rseq . 1) * (seq . 0)))) + ((Rseq . 1) * (seq . 1)) is Element of the carrier of X
((Rseq . 0) * (seq . 0)) + (- ((Rseq . 1) * (seq . 0))) is Element of the carrier of X
(((Rseq . 0) * (seq . 0)) + (- ((Rseq . 1) * (seq . 0)))) + ((Rseq . 1) * (seq . 0)) is Element of the carrier of X
((((Rseq . 0) * (seq . 0)) + (- ((Rseq . 1) * (seq . 0)))) + ((Rseq . 1) * (seq . 0))) + ((Rseq . 1) * (seq . 1)) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . 0) + ((X,(X,seq),Rseq) . (0 + 1)) is Element of the carrier of X
((X,(X,seq,Rseq)) . (0 + 1)) - ((X,(X,seq),Rseq) . (0 + 1)) is Element of the carrier of X
- ((X,(X,seq),Rseq) . (0 + 1)) is Element of the carrier of X
((X,(X,seq,Rseq)) . (0 + 1)) + (- ((X,(X,seq),Rseq) . (0 + 1))) is Element of the carrier of X
((X,(X,seq),Rseq) . (0 + 1)) - ((X,(X,seq),Rseq) . (0 + 1)) is Element of the carrier of X
((X,(X,seq),Rseq) . (0 + 1)) + (- ((X,(X,seq),Rseq) . (0 + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . 0) + (((X,(X,seq),Rseq) . (0 + 1)) - ((X,(X,seq),Rseq) . (0 + 1))) is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . 0) + H₁(X) is Element of the carrier of X
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Rseq ^\ 1 is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Rseq
(Rseq ^\ 1) - Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- Rseq is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive integer set
(- 1) (#) Rseq is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(Rseq ^\ 1) + (- Rseq) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq,Rseq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq),Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq),((Rseq ^\ 1) - Rseq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,(X,seq,Rseq)) . (n + 1) is Element of the carrier of X
(X,(X,seq),Rseq) . (n + 1) is Element of the carrier of X
(X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) . n is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) . n) is Element of the carrier of X
- ((X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) . n) is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + (- ((X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) . n)) is Element of the carrier of X
Rseq - (Rseq ^\ 1) is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- (Rseq ^\ 1) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(- 1) (#) (Rseq ^\ 1) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
Rseq + (- (Rseq ^\ 1)) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(X,(X,seq),(Rseq - (Rseq ^\ 1))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n is Element of the carrier of X
((X,(X,(X,seq),(Rseq - (Rseq ^\ 1)))) . n) + ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
- ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) + (- ((X,(X,seq),Rseq) . (n + 1))) is Element of the carrier of X
(((X,(X,seq,Rseq)) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1))) + ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1)) is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + (- ((X,(X,seq),Rseq) . (n + 1))) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) - (((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1))) is Element of the carrier of X
- (((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1))) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) + (- (((X,(X,seq),Rseq) . (n + 1)) - ((X,(X,seq),Rseq) . (n + 1)))) is Element of the carrier of X
0. X is V80(X) Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) - H₁(X) is Element of the carrier of X
- (0. X) is Element of the carrier of X
((X,(X,seq,Rseq)) . (n + 1)) + (- (0. X)) is Element of the carrier of X
(- 1) (#) (Rseq ^\ 1) is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((- 1) (#) (Rseq ^\ 1)) - (- Rseq) is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- (- Rseq) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(- 1) (#) (- Rseq) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
((- 1) (#) (Rseq ^\ 1)) + (- (- Rseq)) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(X,(X,seq),(((- 1) (#) (Rseq ^\ 1)) - (- Rseq))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),(((- 1) (#) (Rseq ^\ 1)) - (- Rseq)))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),(((- 1) (#) (Rseq ^\ 1)) - (- Rseq)))) . n is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + ((X,(X,(X,seq),(((- 1) (#) (Rseq ^\ 1)) - (- Rseq)))) . n) is Element of the carrier of X
(- 1) (#) ((Rseq ^\ 1) - Rseq) is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(X,(X,seq),((- 1) (#) ((Rseq ^\ 1) - Rseq))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),((- 1) (#) ((Rseq ^\ 1) - Rseq)))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),((- 1) (#) ((Rseq ^\ 1) - Rseq)))) . n is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + ((X,(X,(X,seq),((- 1) (#) ((Rseq ^\ 1) - Rseq)))) . n) is Element of the carrier of X
(- 1) * (X,(X,seq),((Rseq ^\ 1) - Rseq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((- 1) * (X,(X,seq),((Rseq ^\ 1) - Rseq)))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((- 1) * (X,(X,seq),((Rseq ^\ 1) - Rseq)))) . n is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + ((X,((- 1) * (X,(X,seq),((Rseq ^\ 1) - Rseq)))) . n) is Element of the carrier of X
(- 1) * (X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
((- 1) * (X,(X,(X,seq),((Rseq ^\ 1) - Rseq)))) . n is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + (((- 1) * (X,(X,(X,seq),((Rseq ^\ 1) - Rseq)))) . n) is Element of the carrier of X
(- 1) * ((X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) . n) is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + ((- 1) * ((X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) . n)) is Element of the carrier of X
X is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RealUnitarySpace-like UNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
seq is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(X,seq,Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,(X,seq,Rseq),(n + 1)) is Element of the carrier of X
(X,(X,seq,Rseq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq,Rseq)) . (n + 1) is Element of the carrier of X
(X,seq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq),Rseq) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,seq),Rseq) . (n + 1) is Element of the carrier of X
Rseq ^\ 1 is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Rseq
(Rseq ^\ 1) - Rseq is V1() V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- Rseq is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive integer set
(- 1) (#) Rseq is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(Rseq ^\ 1) + (- Rseq) is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(X,(X,seq),((Rseq ^\ 1) - Rseq)) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),((Rseq ^\ 1) - Rseq)),n) is Element of the carrier of X
(X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) is V1() V16() V19( NAT ) V20( the carrier of X) V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(X,(X,seq),((Rseq ^\ 1) - Rseq))) . n is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) - (X,(X,(X,seq),((Rseq ^\ 1) - Rseq)),n) is Element of the carrier of X
- (X,(X,(X,seq),((Rseq ^\ 1) - Rseq)),n) is Element of the carrier of X
((X,(X,seq),Rseq) . (n + 1)) + (- (X,(X,(X,seq),((Rseq ^\ 1) - Rseq)),n)) is Element of the carrier of X