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

(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

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 )