:: CLVECT_2 semantic presentation

REAL is V1() V45() V141() V142() V143() V147() set
NAT is V1() epsilon-transitive epsilon-connected ordinal V141() V142() V143() V144() V145() V146() V147() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V45() V141() V147() set
omega is V1() epsilon-transitive epsilon-connected ordinal V141() V142() V143() V144() V145() V146() V147() set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is complex-valued set
K6(K7(NAT,COMPLEX)) is set
the_set_of_ComplexSequences is V1() set
K7(the_set_of_ComplexSequences,the_set_of_ComplexSequences) is set
K7(K7(the_set_of_ComplexSequences,the_set_of_ComplexSequences),the_set_of_ComplexSequences) is set
K6(K7(K7(the_set_of_ComplexSequences,the_set_of_ComplexSequences),the_set_of_ComplexSequences)) is set
K7(COMPLEX,the_set_of_ComplexSequences) is set
K7(K7(COMPLEX,the_set_of_ComplexSequences),the_set_of_ComplexSequences) is set
K6(K7(K7(COMPLEX,the_set_of_ComplexSequences),the_set_of_ComplexSequences)) is set
Linear_Space_of_ComplexSequences is non empty strict L17()
the carrier of Linear_Space_of_ComplexSequences is V1() set
K6( the carrier of Linear_Space_of_ComplexSequences) is set
the_set_of_l2ComplexSequences is Element of K6( the carrier of Linear_Space_of_ComplexSequences)
K7(the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences) is set
K7(K7(the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences),COMPLEX) is complex-valued set
K6(K7(K7(the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences),COMPLEX)) is set
RAT is V1() V45() V141() V142() V143() V144() V147() set
INT is V1() V45() V141() V142() V143() V144() V145() V147() set
0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() set
1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() 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 V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
K7(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7(NAT,NAT)) is set
1r is V11() Element of COMPLEX
- 1r is V11() Element of COMPLEX
2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
3 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is Element of the carrier of X
k is Element of the carrier of X
r is V11() real ext-real Element of REAL
m1 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
dist ((seq . m),k) is V11() real ext-real Element of REAL
dist (seq2,k) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r is Element of the carrier of X
m1 is Element of the carrier of X
m is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
dist ((seq . m1),r) is V11() real ext-real Element of REAL
seq2 . m1 is Element of the carrier of X
dist ((seq2 . m1),m1) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m1 is Element of the carrier of X
seq . m1 is Element of the carrier of X
dist ((seq2 . m1),m1) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is Element of the carrier of X
r is Element of the carrier of X
k + r is Element of the carrier of X
m1 is Element of the carrier of X
m is V11() real ext-real Element of REAL
m / 2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq + seq2) . m1 is Element of the carrier of X
dist (((seq + seq2) . m1),m1) is V11() real ext-real Element of REAL
seq2 . m1 is Element of the carrier of X
dist ((seq2 . m1),r) is V11() real ext-real Element of REAL
seq . m1 is Element of the carrier of X
(seq . m1) + (seq2 . m1) is Element of the carrier of X
dist (((seq . m1) + (seq2 . m1)),(k + r)) is V11() real ext-real Element of REAL
dist ((seq . m1),k) is V11() real ext-real Element of REAL
(dist ((seq . m1),k)) + (dist ((seq2 . m1),r)) is V11() real ext-real Element of REAL
(m / 2) + (m / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq - seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is Element of the carrier of X
r is Element of the carrier of X
k - r is Element of the carrier of X
m1 is Element of the carrier of X
m is V11() real ext-real Element of REAL
m / 2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq - seq2) . m1 is Element of the carrier of X
dist (((seq - seq2) . m1),m1) is V11() real ext-real Element of REAL
seq2 . m1 is Element of the carrier of X
dist ((seq2 . m1),r) is V11() real ext-real Element of REAL
seq . m1 is Element of the carrier of X
(seq . m1) - (seq2 . m1) is Element of the carrier of X
dist (((seq . m1) - (seq2 . m1)),(k - r)) is V11() real ext-real Element of REAL
dist ((seq . m1),k) is V11() real ext-real Element of REAL
(dist ((seq . m1),k)) + (dist ((seq2 . m1),r)) is V11() real ext-real Element of REAL
(m / 2) + (m / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 V11() set
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq * seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is Element of the carrier of X
seq * k is Element of the carrier of X
r is Element of the carrier of X
|.seq.| is V11() real ext-real Element of REAL
0 / |.seq.| is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m1 / |.seq.| is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
dist ((seq2 . m),k) is V11() real ext-real Element of REAL
|.seq.| * (m1 / |.seq.|) is V11() real ext-real Element of REAL
|.seq.| " is V11() real ext-real Element of REAL
(|.seq.| ") * m1 is V11() real ext-real Element of REAL
|.seq.| * ((|.seq.| ") * m1) is V11() real ext-real Element of REAL
|.seq.| * (|.seq.| ") is V11() real ext-real Element of REAL
(|.seq.| * (|.seq.| ")) * m1 is V11() real ext-real Element of REAL
1 * m1 is V11() real ext-real Element of REAL
seq * (seq2 . m) is Element of the carrier of X
dist ((seq * (seq2 . m)),(seq * k)) is V11() real ext-real Element of REAL
(seq * (seq2 . m)) - (seq * k) is Element of the carrier of X
||.((seq * (seq2 . m)) - (seq * k)).|| is V11() real ext-real Element of REAL
(seq2 . m) - k is Element of the carrier of X
seq * ((seq2 . m) - k) is Element of the carrier of X
||.(seq * ((seq2 . m) - k)).|| is V11() real ext-real Element of REAL
||.((seq2 . m) - k).|| is V11() real ext-real Element of REAL
|.seq.| * ||.((seq2 . m) - k).|| is V11() real ext-real Element of REAL
|.seq.| * (dist ((seq2 . m),k)) is V11() real ext-real Element of REAL
dist ((seq * (seq2 . m)),r) is V11() real ext-real Element of REAL
(seq * seq2) . m is Element of the carrier of X
dist (((seq * seq2) . m),r) is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
dist ((seq2 . m),k) is V11() real ext-real Element of REAL
seq * (seq2 . m) is Element of the carrier of X
dist ((seq * (seq2 . m)),(seq * k)) is V11() real ext-real Element of REAL
0c is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() Element of COMPLEX
0c * (seq2 . m) is Element of the carrier of X
0. X is V64(X) Element of the carrier of X
dist ((0c * (seq2 . m)),H₁(X)) is V11() real ext-real Element of REAL
dist (H₁(X),H₁(X)) is V11() real ext-real Element of REAL
dist ((seq * (seq2 . m)),r) is V11() real ext-real Element of REAL
(seq * seq2) . m is Element of the carrier of X
dist (((seq * seq2) . m),r) is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(- 1r) * seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 + seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is Element of the carrier of X
k + seq is Element of the carrier of X
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq2 + seq) . n is Element of the carrier of X
dist (((seq2 + seq) . n),(k + seq)) is V11() real ext-real Element of REAL
seq2 . n is Element of the carrier of X
(seq2 . n) + seq is Element of the carrier of X
dist (((seq2 . n) + seq),(k + seq)) is V11() real ext-real Element of REAL
dist ((seq2 . n),k) is V11() real ext-real Element of REAL
dist (seq,seq) is V11() real ext-real Element of REAL
(dist ((seq2 . n),k)) + (dist (seq,seq)) is V11() real ext-real Element of REAL
(dist ((seq2 . n),k)) + 0 is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 - seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq is Element of the carrier of X
seq2 + (- seq) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is Element of the carrier of X
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
(seq . m) - seq2 is Element of the carrier of X
||.((seq . m) - seq2).|| is V11() real ext-real Element of REAL
dist ((seq . m),seq2) is V11() real ext-real Element of REAL
seq2 is Element of the carrier of X
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
dist ((seq . m),seq2) is V11() real ext-real Element of REAL
(seq . m) - seq2 is Element of the carrier of X
||.((seq . m) - seq2).|| is V11() real ext-real Element of REAL
seq2 is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is Element of the carrier of X
k is Element of the carrier of X
dist (seq2,k) is V11() real ext-real Element of REAL
4 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(dist (seq2,k)) / 4 is V11() real ext-real Element of REAL
0 / 4 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . r is Element of the carrier of X
dist ((seq . r),k) is V11() real ext-real Element of REAL
seq2 - (seq . r) is Element of the carrier of X
k - (seq . r) is Element of the carrier of X
dist ((seq2 - (seq . r)),(k - (seq . r))) is V11() real ext-real Element of REAL
dist ((seq . r),seq2) is V11() real ext-real Element of REAL
(dist ((seq . r),seq2)) + (dist ((seq . r),k)) is V11() real ext-real Element of REAL
((dist (seq2,k)) / 4) + ((dist (seq2,k)) / 4) is V11() real ext-real Element of REAL
(dist (seq2,k)) / 2 is V11() real ext-real Element of REAL
seq . m1 is Element of the carrier of X
dist ((seq . m1),seq2) is V11() real ext-real Element of REAL
seq2 - (seq . m1) is Element of the carrier of X
k - (seq . m1) is Element of the carrier of X
dist ((seq2 - (seq . m1)),(k - (seq . m1))) is V11() real ext-real Element of REAL
dist ((seq . m1),k) is V11() real ext-real Element of REAL
(dist ((seq . m1),seq2)) + (dist ((seq . m1),k)) is V11() real ext-real Element of REAL
seq2 is Element of the carrier of X
k is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
rng seq2 is set
(X,seq2) is Element of the carrier of X
k is Element of the carrier of X
{k} is V1() set
r is Element of the carrier of X
m1 is V11() real ext-real Element of REAL
m is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
dom seq2 is set
seq2 . n is Element of the carrier of X
dist ((seq2 . n),seq) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . k is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . k is Element of the carrier of X
dom seq2 is set
rng seq2 is set
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) is Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . n is Element of the carrier of X
dist ((seq . n),(X,seq)) is V11() real ext-real Element of REAL
seq2 . n is Element of the carrier of X
dist ((seq2 . n),(X,seq)) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . n is Element of the carrier of X
seq . n is Element of the carrier of X
dist ((seq2 . n),(X,seq)) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) is Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq + seq2)) is Element of the carrier of X
(X,seq2) is Element of the carrier of X
(X,seq) + (X,seq2) is Element of the carrier of X
m is V11() real ext-real Element of REAL
m / 2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m1 is Element of the carrier of X
dist ((seq2 . m1),(X,seq2)) is V11() real ext-real Element of REAL
(seq + seq2) . m1 is Element of the carrier of X
dist (((seq + seq2) . m1),((X,seq) + (X,seq2))) is V11() real ext-real Element of REAL
seq . m1 is Element of the carrier of X
(seq . m1) + (seq2 . m1) is Element of the carrier of X
dist (((seq . m1) + (seq2 . m1)),((X,seq) + (X,seq2))) is V11() real ext-real Element of REAL
dist ((seq . m1),(X,seq)) is V11() real ext-real Element of REAL
(dist ((seq . m1),(X,seq))) + (dist ((seq2 . m1),(X,seq2))) is V11() real ext-real Element of REAL
(m / 2) + (m / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) is Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq - seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq - seq2)) is Element of the carrier of X
(X,seq2) is Element of the carrier of X
(X,seq) - (X,seq2) is Element of the carrier of X
m is V11() real ext-real Element of REAL
m / 2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m1 is Element of the carrier of X
dist ((seq2 . m1),(X,seq2)) is V11() real ext-real Element of REAL
(seq - seq2) . m1 is Element of the carrier of X
dist (((seq - seq2) . m1),((X,seq) - (X,seq2))) is V11() real ext-real Element of REAL
seq . m1 is Element of the carrier of X
(seq . m1) - (seq2 . m1) is Element of the carrier of X
dist (((seq . m1) - (seq2 . m1)),((X,seq) - (X,seq2))) is V11() real ext-real Element of REAL
dist ((seq . m1),(X,seq)) is V11() real ext-real Element of REAL
(dist ((seq . m1),(X,seq))) + (dist ((seq2 . m1),(X,seq2))) is V11() real ext-real Element of REAL
(m / 2) + (m / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 V11() set
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq * seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq * seq2)) is Element of the carrier of X
(X,seq2) is Element of the carrier of X
seq * (X,seq2) is Element of the carrier of X
the epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
seq * (seq2 . m) is Element of the carrier of X
dist ((seq * (seq2 . m)),(seq * (X,seq2))) is V11() real ext-real Element of REAL
0c is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() Element of COMPLEX
0c * (seq2 . m) is Element of the carrier of X
0. X is V64(X) Element of the carrier of X
dist ((0c * (seq2 . m)),H₁(X)) is V11() real ext-real Element of REAL
dist (H₁(X),H₁(X)) is V11() real ext-real Element of REAL
(seq * seq2) . m is Element of the carrier of X
dist (((seq * seq2) . m),(seq * (X,seq2))) is V11() real ext-real Element of REAL
|.seq.| is V11() real ext-real Element of REAL
0 / |.seq.| is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m1 / |.seq.| is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
dist ((seq2 . m),(X,seq2)) is V11() real ext-real Element of REAL
|.seq.| * (m1 / |.seq.|) is V11() real ext-real Element of REAL
|.seq.| " is V11() real ext-real Element of REAL
(|.seq.| ") * m1 is V11() real ext-real Element of REAL
|.seq.| * ((|.seq.| ") * m1) is V11() real ext-real Element of REAL
|.seq.| * (|.seq.| ") is V11() real ext-real Element of REAL
(|.seq.| * (|.seq.| ")) * m1 is V11() real ext-real Element of REAL
1 * m1 is V11() real ext-real Element of REAL
seq * (seq2 . m) is Element of the carrier of X
dist ((seq * (seq2 . m)),(seq * (X,seq2))) is V11() real ext-real Element of REAL
(seq * (seq2 . m)) - (seq * (X,seq2)) is Element of the carrier of X
||.((seq * (seq2 . m)) - (seq * (X,seq2))).|| is V11() real ext-real Element of REAL
(seq2 . m) - (X,seq2) is Element of the carrier of X
seq * ((seq2 . m) - (X,seq2)) is Element of the carrier of X
||.(seq * ((seq2 . m) - (X,seq2))).|| is V11() real ext-real Element of REAL
||.((seq2 . m) - (X,seq2)).|| is V11() real ext-real Element of REAL
|.seq.| * ||.((seq2 . m) - (X,seq2)).|| is V11() real ext-real Element of REAL
|.seq.| * (dist ((seq2 . m),(X,seq2))) is V11() real ext-real Element of REAL
(seq * seq2) . m is Element of the carrier of X
dist (((seq * seq2) . m),(seq * (X,seq2))) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(- seq)) is Element of the carrier of X
(X,seq) is Element of the carrier of X
- (X,seq) is Element of the carrier of X
(- 1r) * seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((- 1r) * seq)) is Element of the carrier of X
(- 1r) * (X,seq) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 + seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq2 + seq)) is Element of the carrier of X
(X,seq2) is Element of the carrier of X
(X,seq2) + seq is Element of the carrier of X
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . n is Element of the carrier of X
dist ((seq2 . n),(X,seq2)) is V11() real ext-real Element of REAL
- seq is Element of the carrier of X
(seq2 . n) - (- seq) is Element of the carrier of X
(X,seq2) - (- seq) is Element of the carrier of X
dist (((seq2 . n) - (- seq)),((X,seq2) - (- seq))) is V11() real ext-real Element of REAL
- (- seq) is Element of the carrier of X
(seq2 . n) + (- (- seq)) is Element of the carrier of X
dist (((seq2 . n) + (- (- seq))),((X,seq2) - (- seq))) is V11() real ext-real Element of REAL
(seq2 . n) + seq is Element of the carrier of X
dist (((seq2 . n) + seq),((X,seq2) - (- seq))) is V11() real ext-real Element of REAL
(X,seq2) + (- (- seq)) is Element of the carrier of X
dist (((seq2 . n) + seq),((X,seq2) + (- (- seq)))) is V11() real ext-real Element of REAL
dist (((seq2 . n) + seq),((X,seq2) + seq)) is V11() real ext-real Element of REAL
(seq2 + seq) . n is Element of the carrier of X
dist (((seq2 + seq) . n),((X,seq2) + seq)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 - seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq2 - seq)) is Element of the carrier of X
(X,seq2) is Element of the carrier of X
(X,seq2) - seq is Element of the carrier of X
- seq is Element of the carrier of X
seq2 + (- seq) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq2 + (- seq))) is Element of the carrier of X
(X,seq2) + (- seq) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
(seq2 . m) - seq is Element of the carrier of X
||.((seq2 . m) - seq).|| is V11() real ext-real Element of REAL
dist ((seq2 . m),seq) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
(seq2 . m) - seq is Element of the carrier of X
||.((seq2 . m) - seq).|| is V11() real ext-real Element of REAL
dist ((seq2 . m),seq) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . 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
seq2 is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . r is V11() real ext-real Element of REAL
seq . r is Element of the carrier of X
||.(seq . r).|| is V11() real ext-real Element of REAL
k . r is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
seq2 is Element of the carrier of X
k is V11() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
(seq . m) - seq2 is Element of the carrier of X
||.((seq . m) - seq2).|| is V11() real ext-real Element of REAL
||.(seq . m).|| is V11() real ext-real Element of REAL
||.seq2.|| is V11() real ext-real Element of REAL
||.(seq . m).|| - ||.seq2.|| is V11() real ext-real Element of REAL
abs (||.(seq . m).|| - ||.seq2.||) is V11() real ext-real Element of REAL
(X,seq) . m is V11() real ext-real Element of REAL
((X,seq) . m) - ||.seq2.|| is V11() real ext-real Element of REAL
abs (((X,seq) . m) - ||.seq2.||) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(X,seq) . m is V11() real ext-real Element of REAL
((X,seq) . m) - ||.seq2.|| is V11() real ext-real Element of REAL
abs (((X,seq) . m) - ||.seq2.||) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
||.seq.|| is V11() real ext-real Element of REAL
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
(X,seq2) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,seq2) is V11() real ext-real Element of REAL
k is V11() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
(seq2 . m) - seq is Element of the carrier of X
||.((seq2 . m) - seq).|| is V11() real ext-real Element of REAL
||.(seq2 . m).|| is V11() real ext-real Element of REAL
||.(seq2 . m).|| - ||.seq.|| is V11() real ext-real Element of REAL
abs (||.(seq2 . m).|| - ||.seq.||) is V11() real ext-real Element of REAL
(X,seq2) . m is V11() real ext-real Element of REAL
((X,seq2) . m) - ||.seq.|| is V11() real ext-real Element of REAL
abs (((X,seq2) . m) - ||.seq.||) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(X,seq2) . m is V11() real ext-real Element of REAL
((X,seq2) . m) - ||.seq.|| is V11() real ext-real Element of REAL
abs (((X,seq2) . m) - ||.seq.||) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
seq2 - seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq2 - seq)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(seq2 - seq)) is V11() real ext-real Element of REAL
k is V11() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
(seq2 . m) - seq is Element of the carrier of X
||.((seq2 . m) - seq).|| is V11() real ext-real Element of REAL
0. X is V64(X) Element of the carrier of X
((seq2 . m) - seq) - H₁(X) is Element of the carrier of X
||.(((seq2 . m) - seq) - H₁(X)).|| is V11() real ext-real Element of REAL
||.H₁(X).|| is V11() real ext-real Element of REAL
||.((seq2 . m) - seq).|| - ||.H₁(X).|| is V11() real ext-real Element of REAL
abs (||.((seq2 . m) - seq).|| - ||.H₁(X).||) is V11() real ext-real Element of REAL
||.((seq2 . m) - seq).|| - 0 is V11() real ext-real Element of REAL
abs (||.((seq2 . m) - seq).|| - 0) is V11() real ext-real Element of REAL
(seq2 - seq) . m is Element of the carrier of X
||.((seq2 - seq) . m).|| is V11() real ext-real Element of REAL
||.((seq2 - seq) . m).|| - 0 is V11() real ext-real Element of REAL
abs (||.((seq2 - seq) . m).|| - 0) is V11() real ext-real Element of REAL
(X,(seq2 - seq)) . m is V11() real ext-real Element of REAL
((X,(seq2 - seq)) . m) - 0 is V11() real ext-real Element of REAL
abs (((X,(seq2 - seq)) . m) - 0) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is Element of the carrier of X
k is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k . r is V11() real ext-real Element of REAL
seq . r is Element of the carrier of X
dist ((seq . r),seq2) is V11() real ext-real Element of REAL
k is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
r is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k . m1 is V11() real ext-real Element of REAL
seq . m1 is Element of the carrier of X
dist ((seq . m1),seq2) is V11() real ext-real Element of REAL
r . m1 is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
(X,seq2,seq) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
k is V11() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
dist ((seq2 . m),seq) is V11() real ext-real Element of REAL
(dist ((seq2 . m),seq)) - 0 is V11() real ext-real Element of REAL
abs ((dist ((seq2 . m),seq)) - 0) is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(X,seq2,seq) . m is V11() real ext-real Element of REAL
((X,seq2,seq) . m) - 0 is V11() real ext-real Element of REAL
abs (((X,seq2,seq) . m) - 0) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(X,seq2,seq) . m is V11() real ext-real Element of REAL
((X,seq2,seq) . m) - 0 is V11() real ext-real Element of REAL
abs (((X,seq2,seq) . m) - 0) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
(X,seq2,seq) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,seq2,seq) is V11() real ext-real Element of REAL
k is V11() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
dist ((seq2 . m),seq) is V11() real ext-real Element of REAL
(dist ((seq2 . m),seq)) - 0 is V11() real ext-real Element of REAL
abs ((dist ((seq2 . m),seq)) - 0) is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(X,seq2,seq) . m is V11() real ext-real Element of REAL
((X,seq2,seq) . m) - 0 is V11() real ext-real Element of REAL
abs (((X,seq2,seq) . m) - 0) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq + seq2 is Element of the carrier of X
||.(seq + seq2).|| is V11() real ext-real Element of REAL
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,r) is Element of the carrier of X
k + r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(k + r)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(k + r)) is V11() real ext-real Element of REAL
(X,(k + r)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq + seq2 is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,r) is Element of the carrier of X
k + r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(k + r) - (seq + seq2) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((k + r) - (seq + seq2))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,((k + r) - (seq + seq2))) is V11() real ext-real Element of REAL
(X,(k + r)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq - seq2 is Element of the carrier of X
||.(seq - seq2).|| is V11() real ext-real Element of REAL
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,r) is Element of the carrier of X
k - r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(k - r)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(k - r)) is V11() real ext-real Element of REAL
(X,(k - r)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq - seq2 is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,r) is Element of the carrier of X
k - r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(k - r) - (seq - seq2) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((k - r) - (seq - seq2))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,((k - r) - (seq - seq2))) is V11() real ext-real Element of REAL
(X,(k - r)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V11() set
seq2 * seq is Element of the carrier of X
||.(seq2 * seq).|| is V11() real ext-real Element of REAL
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
seq2 * k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq2 * k)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(seq2 * k)) is V11() real ext-real Element of REAL
(X,(seq2 * k)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V11() set
seq2 * seq is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
seq2 * k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(seq2 * k) - (seq2 * seq) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((seq2 * k) - (seq2 * seq))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,((seq2 * k) - (seq2 * seq))) is V11() real ext-real Element of REAL
(X,(seq2 * k)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
- seq is Element of the carrier of X
||.(- seq).|| is V11() real ext-real Element of REAL
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
- seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(- seq2)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(- seq2)) is V11() real ext-real Element of REAL
(X,(- seq2)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
- seq is Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
- seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(- seq2) - (- seq) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((- seq2) - (- seq))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,((- seq2) - (- seq))) is V11() real ext-real Element of REAL
(X,(- seq2)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq + seq2 is Element of the carrier of X
||.(seq + seq2).|| is V11() real ext-real Element of REAL
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
k + seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(k + seq2)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(k + seq2)) is V11() real ext-real Element of REAL
(X,(k + seq2)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq + seq2 is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
k + seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(k + seq2) - (seq + seq2) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((k + seq2) - (seq + seq2))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,((k + seq2) - (seq + seq2))) is V11() real ext-real Element of REAL
(X,(k + seq2)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq - seq2 is Element of the carrier of X
||.(seq - seq2).|| is V11() real ext-real Element of REAL
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
k - seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(k - seq2)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(k - seq2)) is V11() real ext-real Element of REAL
- seq2 is Element of the carrier of X
k + (- seq2) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(k + (- seq2))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(k + (- seq2))) is V11() real ext-real Element of REAL
seq + (- seq2) is Element of the carrier of X
||.(seq + (- seq2)).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq - seq2 is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
k - seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(k - seq2) - (seq - seq2) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((k - seq2) - (seq - seq2))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,((k - seq2) - (seq - seq2))) is V11() real ext-real Element of REAL
- seq2 is Element of the carrier of X
k + (- seq2) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + (- seq2) is Element of the carrier of X
(k + (- seq2)) - (seq + (- seq2)) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((k + (- seq2)) - (seq + (- seq2)))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,((k + (- seq2)) - (seq + (- seq2)))) is V11() real ext-real Element of REAL
(k - seq2) - (seq + (- seq2)) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,((k - seq2) - (seq + (- seq2)))) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,((k - seq2) - (seq + (- seq2)))) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq + seq2 is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,r) is Element of the carrier of X
k + r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(k + r),(seq + seq2)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(k + r),(seq + seq2)) is V11() real ext-real Element of REAL
(X,(k + r)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq - seq2 is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,r) is Element of the carrier of X
k - r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(k - r),(seq - seq2)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(k - r),(seq - seq2)) is V11() real ext-real Element of REAL
(X,(k - r)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V11() set
seq2 * seq is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
seq2 * k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(seq2 * k),(seq2 * seq)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(seq2 * k),(seq2 * seq)) is V11() real ext-real Element of REAL
(X,(seq2 * k)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is Element of the carrier of X
seq + seq2 is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
k + seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,(k + seq2),(seq + seq2)) is V1() Relation-like NAT -defined REAL -valued V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim (X,(k + seq2),(seq + seq2)) is V11() real ext-real Element of REAL
(X,(k + seq2)) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq2 is V11() real ext-real Element of REAL
seq is Element of the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not seq2 <= ||.(seq - b₁).|| } is set
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : S₁[b₁] } is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq - b₁).|| <= seq2 } is set
{ b₁ where b₁ is Element of the carrier of X : S₁[b₁] } is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq - b₁).|| = seq2 } is set
{ b₁ where b₁ is Element of the carrier of X : S₁[b₁] } is set
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not k <= ||.(seq2 - b₁).|| } is set
r is Element of the carrier of X
seq2 - r is Element of the carrier of X
||.(seq2 - r).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
dist (seq2,seq) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not k <= ||.(seq2 - b₁).|| } is set
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is V11() real ext-real Element of REAL
(X,seq,seq2) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not seq2 <= ||.(seq - b₁).|| } is set
dist (seq,seq) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
k is Element of the carrier of X
dist (seq,k) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
(X,seq2,r) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not r <= ||.(seq2 - b₁).|| } is set
2 * r is V11() real ext-real Element of REAL
dist (seq2,k) is V11() real ext-real Element of REAL
r + r is V11() real ext-real Element of REAL
r + (dist (seq2,k)) is V11() real ext-real Element of REAL
dist (seq,seq2) is V11() real ext-real Element of REAL
(dist (seq,seq2)) + (dist (seq2,k)) is V11() real ext-real Element of REAL
dist (seq2,seq) is V11() real ext-real Element of REAL
(dist (seq2,seq)) + (dist (seq2,k)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
k is Element of the carrier of X
seq - k is Element of the carrier of X
seq2 - k is Element of the carrier of X
r is V11() real ext-real Element of REAL
(X,seq2,r) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not r <= ||.(seq2 - b₁).|| } is set
(X,(seq2 - k),r) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : not r <= ||.((seq2 - k) - b₁).|| } is set
dist (seq2,seq) is V11() real ext-real Element of REAL
dist ((seq2 - k),(seq - k)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
0. X is V64(X) Element of the carrier of X
seq is Element of the carrier of X
seq2 is Element of the carrier of X
seq - seq2 is Element of the carrier of X
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not k <= ||.(seq2 - b₁).|| } is set
(X,(0. X),k) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : not k <= ||.((0. X) - b₁).|| } is set
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
- seq is Element of the carrier of X
(- seq) + seq2 is Element of the carrier of X
||.((- seq) + seq2).|| is V11() real ext-real Element of REAL
- (seq - seq2) is Element of the carrier of X
||.(- (seq - seq2)).|| is V11() real ext-real Element of REAL
H₁(X) - (seq - seq2) is Element of the carrier of X
||.(H₁(X) - (seq - seq2)).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not k <= ||.(seq2 - b₁).|| } is set
r is V11() real ext-real Element of REAL
(X,seq2,r) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : not r <= ||.(seq2 - b₁).|| } is set
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq2 - b₁).|| <= k } is set
r is Element of the carrier of X
seq2 - r is Element of the carrier of X
||.(seq2 - r).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
dist (seq2,seq) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq2 - b₁).|| <= k } is set
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is V11() real ext-real Element of REAL
(X,seq,seq2) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq - b₁).|| <= seq2 } is set
dist (seq,seq) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not k <= ||.(seq2 - b₁).|| } is set
(X,seq2,k) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : ||.(seq2 - b₁).|| <= k } is set
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq2 - b₁).|| = k } is set
r is Element of the carrier of X
seq2 - r is Element of the carrier of X
||.(seq2 - r).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
dist (seq2,seq) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq2 - b₁).|| = k } is set
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is Element of the carrier of X
k is V11() real ext-real Element of REAL
(X,seq2,k) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq2 - b₁).|| = k } is set
(X,seq2,k) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : ||.(seq2 - b₁).|| <= k } is set
seq2 - seq is Element of the carrier of X
||.(seq2 - seq).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is V11() real ext-real Element of REAL
(X,seq,seq2) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not seq2 <= ||.(seq - b₁).|| } is set
(X,seq,seq2) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : ||.(seq - b₁).|| <= seq2 } is set
k is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is V11() real ext-real Element of REAL
(X,seq,seq2) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : ||.(seq - b₁).|| = seq2 } is set
(X,seq,seq2) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : ||.(seq - b₁).|| <= seq2 } is set
k is Element of the carrier of X
seq - k is Element of the carrier of X
||.(seq - k).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
seq is Element of the carrier of X
seq2 is V11() real ext-real Element of REAL
(X,seq,seq2) is Element of K6( the carrier of X)
K6( the carrier of X) is set
{ b₁ where b₁ is Element of the carrier of X : not seq2 <= ||.(seq - b₁).|| } is set
(X,seq,seq2) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : ||.(seq - b₁).|| = seq2 } is set
(X,seq,seq2) \/ (X,seq,seq2) is Element of K6( the carrier of X)
(X,seq,seq2) is Element of K6( the carrier of X)
{ b₁ where b₁ is Element of the carrier of X : ||.(seq - b₁).|| <= seq2 } is set
k is Element of the carrier of X
seq - k is Element of the carrier of X
||.(seq - k).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V11() real ext-real Element of REAL
k is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . r is Element of the carrier of X
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
dist ((seq . r),(seq . m1)) is V11() real ext-real Element of REAL
dist ((seq . r),(seq . r)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
(seq . m1) - (seq . m) is Element of the carrier of X
||.((seq . m1) - (seq . m)).|| is V11() real ext-real Element of REAL
dist ((seq . m1),(seq . m)) is V11() real ext-real Element of REAL
seq2 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
dist ((seq . m1),(seq . m)) is V11() real ext-real Element of REAL
(seq . m1) - (seq . m) is Element of the carrier of X
||.((seq . m1) - (seq . m)).|| is V11() real ext-real Element of REAL
seq2 is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
k / 2 is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r + m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq + seq2) . n is Element of the carrier of X
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq + seq2) . m is Element of the carrier of X
dist (((seq + seq2) . n),((seq + seq2) . m)) is V11() real ext-real Element of REAL
seq2 . n is Element of the carrier of X
seq2 . m is Element of the carrier of X
dist ((seq2 . n),(seq2 . m)) is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
(seq . n) + (seq2 . n) is Element of the carrier of X
dist (((seq . n) + (seq2 . n)),((seq + seq2) . m)) is V11() real ext-real Element of REAL
seq . m is Element of the carrier of X
(seq . m) + (seq2 . m) is Element of the carrier of X
dist (((seq . n) + (seq2 . n)),((seq . m) + (seq2 . m))) is V11() real ext-real Element of REAL
dist ((seq . n),(seq . m)) is V11() real ext-real Element of REAL
(dist ((seq . n),(seq . m))) + (dist ((seq2 . n),(seq2 . m))) is V11() real ext-real Element of REAL
(k / 2) + (k / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq - seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
k / 2 is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r + m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq - seq2) . n is Element of the carrier of X
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq - seq2) . m is Element of the carrier of X
dist (((seq - seq2) . n),((seq - seq2) . m)) is V11() real ext-real Element of REAL
seq2 . n is Element of the carrier of X
seq2 . m is Element of the carrier of X
dist ((seq2 . n),(seq2 . m)) is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
(seq . n) - (seq2 . n) is Element of the carrier of X
dist (((seq . n) - (seq2 . n)),((seq - seq2) . m)) is V11() real ext-real Element of REAL
seq . m is Element of the carrier of X
(seq . m) - (seq2 . m) is Element of the carrier of X
dist (((seq . n) - (seq2 . n)),((seq . m) - (seq2 . m))) is V11() real ext-real Element of REAL
dist ((seq . n),(seq . m)) is V11() real ext-real Element of REAL
(dist ((seq . n),(seq . m))) + (dist ((seq2 . n),(seq2 . m))) is V11() real ext-real Element of REAL
(k / 2) + (k / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 V11() set
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq * seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
|.seq.| is V11() real ext-real Element of REAL
0 / |.seq.| is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
k / |.seq.| is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
seq2 . n is Element of the carrier of X
dist ((seq2 . m),(seq2 . n)) is V11() real ext-real Element of REAL
|.seq.| * (k / |.seq.|) is V11() real ext-real Element of REAL
|.seq.| " is V11() real ext-real Element of REAL
(|.seq.| ") * k is V11() real ext-real Element of REAL
|.seq.| * ((|.seq.| ") * k) is V11() real ext-real Element of REAL
|.seq.| * (|.seq.| ") is V11() real ext-real Element of REAL
(|.seq.| * (|.seq.| ")) * k is V11() real ext-real Element of REAL
1 * k is V11() real ext-real Element of REAL
seq * (seq2 . m) is Element of the carrier of X
seq * (seq2 . n) is Element of the carrier of X
dist ((seq * (seq2 . m)),(seq * (seq2 . n))) is V11() real ext-real Element of REAL
(seq * (seq2 . m)) - (seq * (seq2 . n)) is Element of the carrier of X
||.((seq * (seq2 . m)) - (seq * (seq2 . n))).|| is V11() real ext-real Element of REAL
(seq2 . m) - (seq2 . n) is Element of the carrier of X
seq * ((seq2 . m) - (seq2 . n)) is Element of the carrier of X
||.(seq * ((seq2 . m) - (seq2 . n))).|| is V11() real ext-real Element of REAL
||.((seq2 . m) - (seq2 . n)).|| is V11() real ext-real Element of REAL
|.seq.| * ||.((seq2 . m) - (seq2 . n)).|| is V11() real ext-real Element of REAL
|.seq.| * (dist ((seq2 . m),(seq2 . n))) is V11() real ext-real Element of REAL
(seq * seq2) . m is Element of the carrier of X
dist (((seq * seq2) . m),(seq * (seq2 . n))) is V11() real ext-real Element of REAL
(seq * seq2) . n is Element of the carrier of X
dist (((seq * seq2) . m),((seq * seq2) . n)) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
seq2 . n is Element of the carrier of X
dist ((seq2 . m),(seq2 . n)) is V11() real ext-real Element of REAL
seq * (seq2 . m) is Element of the carrier of X
seq * (seq2 . n) is Element of the carrier of X
dist ((seq * (seq2 . m)),(seq * (seq2 . n))) is V11() real ext-real Element of REAL
0. X is V64(X) Element of the carrier of X
0c is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() Element of COMPLEX
0c * (seq2 . n) is Element of the carrier of X
dist (H₂(X),(0c * (seq2 . n))) is V11() real ext-real Element of REAL
dist (H₂(X),H₂(X)) is V11() real ext-real Element of REAL
(seq * seq2) . m is Element of the carrier of X
dist (((seq * seq2) . m),(seq * (seq2 . n))) is V11() real ext-real Element of REAL
(seq * seq2) . n is Element of the carrier of X
dist (((seq * seq2) . m),((seq * seq2) . n)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(- 1r) * seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 + seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq2 + seq) . m is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq2 + seq) . n is Element of the carrier of X
dist (((seq2 + seq) . m),((seq2 + seq) . n)) is V11() real ext-real Element of REAL
seq2 . m is Element of the carrier of X
(seq2 . m) + seq is Element of the carrier of X
seq2 . n is Element of the carrier of X
(seq2 . n) + seq is Element of the carrier of X
dist (((seq2 . m) + seq),((seq2 . n) + seq)) is V11() real ext-real Element of REAL
dist ((seq2 . m),(seq2 . n)) is V11() real ext-real Element of REAL
dist (seq,seq) is V11() real ext-real Element of REAL
(dist ((seq2 . m),(seq2 . n))) + (dist (seq,seq)) is V11() real ext-real Element of REAL
(dist ((seq2 . m),(seq2 . n))) + 0 is V11() real ext-real Element of REAL
dist (((seq2 + seq) . m),((seq2 . n) + seq)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 - seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq is Element of the carrier of X
seq2 + (- seq) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is Element of the carrier of X
k is V11() real ext-real Element of REAL
k / 2 is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . n is Element of the carrier of X
dist ((seq . m),(seq . n)) is V11() real ext-real Element of REAL
dist ((seq . m),seq2) is V11() real ext-real Element of REAL
dist ((seq . n),seq2) is V11() real ext-real Element of REAL
dist (seq2,(seq . n)) is V11() real ext-real Element of REAL
(dist ((seq . m),seq2)) + (dist (seq2,(seq . n))) is V11() real ext-real Element of REAL
(k / 2) + (k / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V11() real ext-real Element of REAL
k is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . r is Element of the carrier of X
dist ((seq . r),(seq . r)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
seq . m is Element of the carrier of X
dist ((seq2 . m),(seq . m)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
r is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
k . m is Element of the carrier of X
dist ((seq . m),(k . m)) is V11() real ext-real Element of REAL
seq2 . m is Element of the carrier of X
dist ((seq2 . m),(k . m)) is V11() real ext-real Element of REAL
dist ((seq . m),(seq2 . m)) is V11() real ext-real Element of REAL
(dist ((seq . m),(seq2 . m))) + (dist ((seq2 . m),(k . m))) is V11() real ext-real Element of REAL
(r / 2) + (r / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
seq2 . m is Element of the carrier of X
(seq . m) - (seq2 . m) is Element of the carrier of X
||.((seq . m) - (seq2 . m)).|| is V11() real ext-real Element of REAL
dist ((seq . m),(seq2 . m)) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
seq2 . m is Element of the carrier of X
dist ((seq . m),(seq2 . m)) is V11() real ext-real Element of REAL
(seq . m) - (seq2 . m) is Element of the carrier of X
||.((seq . m) - (seq2 . m)).|| is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
seq2 . m is Element of the carrier of X
dist ((seq . m),(seq2 . m)) is V11() real ext-real Element of REAL
dist ((seq . m),(seq . m)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
k / 3 is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r + m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . n is Element of the carrier of X
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
dist ((seq2 . n),(seq2 . m)) is V11() real ext-real Element of REAL
seq . n is Element of the carrier of X
seq . m is Element of the carrier of X
dist ((seq . n),(seq . m)) is V11() real ext-real Element of REAL
dist ((seq2 . n),(seq . m)) is V11() real ext-real Element of REAL
dist ((seq2 . n),(seq . n)) is V11() real ext-real Element of REAL
(dist ((seq2 . n),(seq . n))) + (dist ((seq . n),(seq . m))) is V11() real ext-real Element of REAL
dist ((seq . n),(seq2 . n)) is V11() real ext-real Element of REAL
(k / 3) + (k / 3) is V11() real ext-real Element of REAL
dist ((seq . m),(seq2 . m)) is V11() real ext-real Element of REAL
(dist ((seq2 . n),(seq . m))) + (dist ((seq . m),(seq2 . m))) is V11() real ext-real Element of REAL
((k / 3) + (k / 3)) + (k / 3) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
k / 2 is V11() real ext-real Element of REAL
(X,seq) is Element of the carrier of X
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r + m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . n is Element of the carrier of X
seq2 . n is Element of the carrier of X
dist ((seq . n),(seq2 . n)) is V11() real ext-real Element of REAL
dist ((seq2 . n),(X,seq)) is V11() real ext-real Element of REAL
dist ((seq2 . n),(seq . n)) is V11() real ext-real Element of REAL
dist ((seq . n),(X,seq)) is V11() real ext-real Element of REAL
(dist ((seq2 . n),(seq . n))) + (dist ((seq . n),(X,seq))) is V11() real ext-real Element of REAL
(k / 2) + (k / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,k) is Element of the carrier of X
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
k . m is Element of the carrier of X
dist ((seq2 . m),(k . m)) is V11() real ext-real Element of REAL
dist ((k . m),seq) is V11() real ext-real Element of REAL
dist ((k . m),(seq2 . m)) is V11() real ext-real Element of REAL
dist ((seq2 . m),seq) is V11() real ext-real Element of REAL
(dist ((k . m),(seq2 . m))) + (dist ((seq2 . m),seq)) is V11() real ext-real Element of REAL
(r / 2) + (r / 2) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
the carrier of X is V1() set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq + seq2) . m1 is Element of the carrier of X
||.((seq + seq2) . m1).|| is V11() real ext-real Element of REAL
seq . m1 is Element of the carrier of X
seq2 . m1 is Element of the carrier of X
(seq . m1) + (seq2 . m1) is Element of the carrier of X
||.((seq . m1) + (seq2 . m1)).|| is V11() real ext-real Element of REAL
||.(seq . m1).|| is V11() real ext-real Element of REAL
||.(seq2 . m1).|| is V11() real ext-real Element of REAL
||.(seq . m1).|| + ||.(seq2 . m1).|| is V11() real ext-real Element of REAL
r + k is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(- seq) . k is Element of the carrier of X
||.((- seq) . k).|| is V11() real ext-real Element of REAL
seq . k is Element of the carrier of X
- (seq . k) is Element of the carrier of X
||.(- (seq . k)).|| is V11() real ext-real Element of REAL
||.(seq . k).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq - seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + (- seq2) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 V11() set
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq * seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V11() real ext-real Element of REAL
|.seq.| is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq * seq2) . r is Element of the carrier of X
||.((seq * seq2) . r).|| is V11() real ext-real Element of REAL
seq2 . r is Element of the carrier of X
seq * (seq2 . r) is Element of the carrier of X
||.(seq * (seq2 . r)).|| is V11() real ext-real Element of REAL
||.(seq2 . r).|| is V11() real ext-real Element of REAL
|.seq.| * ||.(seq2 . r).|| is V11() real ext-real Element of REAL
|.seq.| * k is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq * seq2) . r is Element of the carrier of X
||.((seq * seq2) . r).|| is V11() real ext-real Element of REAL
seq2 . r is Element of the carrier of X
0c is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() Element of COMPLEX
0c * (seq2 . r) is Element of the carrier of X
||.(0c * (seq2 . r)).|| is V11() real ext-real Element of REAL
0. X is V64(X) Element of the carrier of X
||.H₂(X).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is Element of the carrier of X
0. X is V64(X) Element of the carrier of X
k is V11() real ext-real set
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
||.(seq . m1).|| is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
||.seq2.|| is V11() real ext-real Element of REAL
k is V11() real ext-real set
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
||.(seq . m1).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k is V11() real ext-real Element of REAL
seq . (seq2 + 1) is Element of the carrier of X
||.(seq . (seq2 + 1)).|| is V11() real ext-real Element of REAL
||.(seq . (seq2 + 1)).|| + 1 is V11() real ext-real Element of REAL
r 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 V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
||.(seq . m1).|| is V11() real ext-real Element of REAL
||.(seq . m1).|| + 0 is V11() real ext-real Element of REAL
k + 1 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
||.(seq . m1).|| is V11() real ext-real Element of REAL
k + 0 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
seq . 0 is Element of the carrier of X
||.(seq . 0).|| is V11() real ext-real Element of REAL
||.(seq . 0).|| + 1 is V11() real ext-real Element of REAL
seq2 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 V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . k is Element of the carrier of X
||.(seq . k).|| is V11() real ext-real Element of REAL
||.(seq . k).|| + 0 is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is Element of the carrier of X
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
||.seq2.|| is V11() real ext-real Element of REAL
||.seq2.|| + 1 is V11() real ext-real Element of REAL
r 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 V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m1 is Element of the carrier of X
(seq . m1) - seq2 is Element of the carrier of X
||.((seq . m1) - seq2).|| is V11() real ext-real Element of REAL
||.(seq . m1).|| is V11() real ext-real Element of REAL
||.(seq . m1).|| - ||.seq2.|| is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m1 + r is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
0 + r is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . n is Element of the carrier of X
||.(seq . n).|| is V11() real ext-real Element of REAL
m1 + 0 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
r is V11() real ext-real Element of REAL
r + 1 is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m is Element of the carrier of X
seq2 . m is Element of the carrier of X
dist ((seq . m),(seq2 . m)) is V11() real ext-real Element of REAL
(seq2 . m) - (seq . m) is Element of the carrier of X
||.((seq2 . m) - (seq . m)).|| is V11() real ext-real Element of REAL
||.(seq2 . m).|| is V11() real ext-real Element of REAL
||.(seq . m).|| is V11() real ext-real Element of REAL
||.(seq2 . m).|| - ||.(seq . m).|| is V11() real ext-real Element of REAL
||.(seq . m).|| + 1 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
||.(seq2 . m).|| is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
m + m1 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
0 + m1 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
||.(seq2 . m).|| is V11() real ext-real Element of REAL
m + 0 is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V1() Relation-like NAT -defined NAT -valued V21() V26( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
seq * k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
r is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
k . m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . (k . m) is Element of the carrier of X
||.(seq2 . m).|| is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
||.(seq2 . m).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V1() Relation-like NAT -defined NAT -valued V21() V26( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
seq * k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
r is Element of the carrier of X
m1 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k . m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
seq . (k . m) is Element of the carrier of X
(seq2 . m) - r is Element of the carrier of X
||.((seq2 . m) - r).|| is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq) is Element of the carrier of X
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(X,seq2) is Element of the carrier of X
k is V1() Relation-like NAT -defined NAT -valued V21() V26( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
seq2 * k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k . n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . n is Element of the carrier of X
seq2 . (k . n) is Element of the carrier of X
dist ((seq . n),(X,seq2)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
k is V1() Relation-like NAT -defined NAT -valued V21() V26( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K6(K7(NAT,NAT))
seq * k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k . n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
k . m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . n is Element of the carrier of X
seq . (k . n) is Element of the carrier of X
seq2 . m is Element of the carrier of X
seq . (k . m) is Element of the carrier of X
dist ((seq2 . n),(seq2 . m)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq + seq2) ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq + seq2
seq ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
seq2 ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
(seq ^\ k) + (seq2 ^\ k) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
((seq + seq2) ^\ k) . r is Element of the carrier of X
r + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq + seq2) . (r + k) is Element of the carrier of X
seq . (r + k) is Element of the carrier of X
seq2 . (r + k) is Element of the carrier of X
(seq . (r + k)) + (seq2 . (r + k)) is Element of the carrier of X
(seq ^\ k) . r is Element of the carrier of X
((seq ^\ k) . r) + (seq2 . (r + k)) is Element of the carrier of X
(seq2 ^\ k) . r is Element of the carrier of X
((seq ^\ k) . r) + ((seq2 ^\ k) . r) is Element of the carrier of X
((seq ^\ k) + (seq2 ^\ k)) . r is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(- seq) ^\ seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of - seq
seq ^\ seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
- (seq ^\ seq2) is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
((- seq) ^\ seq2) . k is Element of the carrier of X
k + seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(- seq) . (k + seq2) is Element of the carrier of X
seq . (k + seq2) is Element of the carrier of X
- (seq . (k + seq2)) is Element of the carrier of X
(seq ^\ seq2) . k is Element of the carrier of X
- ((seq ^\ seq2) . k) is Element of the carrier of X
(- (seq ^\ seq2)) . k is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq - seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq - seq2) ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq - seq2
seq ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
seq2 ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
(seq ^\ k) - (seq2 ^\ k) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq + (- seq2) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(seq + (- seq2)) ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq + (- seq2)
(- seq2) ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of - seq2
(seq ^\ k) + ((- seq2) ^\ k) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
- (seq2 ^\ k) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
(seq ^\ k) + (- (seq2 ^\ k)) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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 V11() set
seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq * seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq * seq2) ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq * seq2
seq2 ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
seq * (seq2 ^\ k) is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
((seq * seq2) ^\ k) . r is Element of the carrier of X
r + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq * seq2) . (r + k) is Element of the carrier of X
seq2 . (r + k) is Element of the carrier of X
seq * (seq2 . (r + k)) is Element of the carrier of X
(seq2 ^\ k) . r is Element of the carrier of X
seq * ((seq2 ^\ k) . r) is Element of the carrier of X
(seq * (seq2 ^\ k)) . r is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq ^\ seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
(X,(seq ^\ seq2)) is Element of the carrier of X
(X,seq) is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
r is Element of the carrier of X
m is V11() real ext-real Element of REAL
m1 is Element of the carrier of X
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(n + k) + m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 - k is V11() real ext-real Element of REAL
l2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n + l2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m2 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . m2 is Element of the carrier of X
(seq . m2) - m1 is Element of the carrier of X
||.((seq . m2) - m1).|| is V11() real ext-real Element of REAL
seq2 . m1 is Element of the carrier of X
(seq2 . m1) - m1 is Element of the carrier of X
||.((seq2 . m1) - m1).|| is V11() real ext-real Element of REAL
m1 is Element of the carrier of X
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . n is Element of the carrier of X
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq2 . m is Element of the carrier of X
dist ((seq2 . n),(seq2 . m)) is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(m1 + k) + m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n - k is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 + m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
l2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(m1 + k) + m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m - k is V11() real ext-real Element of REAL
m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m1 + m2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
l3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
l2 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
l3 + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . l2 is Element of the carrier of X
seq . l3 is Element of the carrier of X
dist ((seq . l2),(seq . l3)) is V11() real ext-real Element of REAL
dist ((seq2 . n),(seq . l3)) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq ^\ seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is V1() Relation-like NAT -defined the carrier of X -valued 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 non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
seq2 ^\ k is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq2
r is V11() real ext-real Element of REAL
m1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(seq ^\ k) . n is Element of the carrier of X
(seq2 ^\ k) . n is Element of the carrier of X
dist (((seq ^\ k) . n),((seq2 ^\ k) . n)) is V11() real ext-real Element of REAL
n + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq . (n + k) is Element of the carrier of X
seq2 . (n + k) is Element of the carrier of X
dist ((seq . (n + k)),(seq2 . (n + k))) is V11() real ext-real Element of REAL
dist (((seq ^\ k) . n),(seq2 . (n + k))) is V11() real ext-real Element of REAL
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq ^\ seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))
seq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
seq ^\ seq2 is V1() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) subsequence of seq
X is non empty V83() V108() V109() V110() V129() V130() V131() V132() ComplexUnitarySpace-like CUNITSTR
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() Relation-like NAT -defined the carrier of X -valued V21() V26( NAT ) V30( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))