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

dist (H

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

dist (H

(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

||.(((seq2 . m) - seq) - H

||.H

||.((seq2 . m) - seq).|| - ||.H

abs (||.((seq2 . m) - seq).|| - ||.H

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