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