:: BHSP_3 semantic presentation

REAL is V11() V44() V127() V128() V129() V133() set

NAT is V11() epsilon-transitive epsilon-connected ordinal V127() V128() V129() V130() V131() V132() V133() Element of K19(REAL)

K19(REAL) is set

0 is V11() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V127() V128() V129() V130() V131() V132() V133() set

1 is V11() ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

K81(0,1) is V11() V127() V128() V129() V130() V131() V132() set

INT is V11() V44() V127() V128() V129() V130() V131() V133() set

COMPLEX is V11() V44() V127() V133() set

omega is V11() epsilon-transitive epsilon-connected ordinal V127() V128() V129() V130() V131() V132() V133() set

K19(omega) is set

K19(NAT) is set

K20(NAT,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(NAT,REAL)) is set

RAT is V11() V44() V127() V128() V129() V130() V133() set

K20(NAT,NAT) is V5( INT ) V5( RAT ) complex-valued ext-real-valued real-valued natural-valued set

K19(K20(NAT,NAT)) is set

0 is V11() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

- 1 is ext-real non positive V31() real Element of REAL

2 is V11() ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

3 is V11() ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is ext-real V31() real Element of REAL

k is V11() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . r is Element of the U1 of X

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m1 is Element of the U1 of X

dist ((seq . r),(seq . m1)) is ext-real V31() real Element of REAL

dist ((seq . r),(seq . r)) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is ext-real V31() real Element of REAL

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m1 is Element of the U1 of X

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m is Element of the U1 of X

(seq . m1) - (seq . m) is Element of the U1 of X

||.((seq . m1) - (seq . m)).|| is ext-real V31() real Element of REAL

dist ((seq . m1),(seq . m)) is ext-real V31() real Element of REAL

seq2 is ext-real V31() real Element of REAL

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m1 is Element of the U1 of X

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m is Element of the U1 of X

dist ((seq . m1),(seq . m)) is ext-real V31() real Element of REAL

(seq . m1) - (seq . m) is Element of the U1 of X

||.((seq . m1) - (seq . m)).|| is ext-real V31() real Element of REAL

seq2 is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq + seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

k / 2 is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r + m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq + seq2) . n is Element of the U1 of X

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq + seq2) . m is Element of the U1 of X

dist (((seq + seq2) . n),((seq + seq2) . m)) is ext-real V31() real Element of REAL

seq2 . n is Element of the U1 of X

seq2 . m is Element of the U1 of X

dist ((seq2 . n),(seq2 . m)) is ext-real V31() real Element of REAL

seq . n is Element of the U1 of X

(seq . n) + (seq2 . n) is Element of the U1 of X

dist (((seq . n) + (seq2 . n)),((seq + seq2) . m)) is ext-real V31() real Element of REAL

seq . m is Element of the U1 of X

(seq . m) + (seq2 . m) is Element of the U1 of X

dist (((seq . n) + (seq2 . n)),((seq . m) + (seq2 . m))) is ext-real V31() real Element of REAL

dist ((seq . n),(seq . m)) is ext-real V31() real Element of REAL

(dist ((seq . n),(seq . m))) + (dist ((seq2 . n),(seq2 . m))) is ext-real V31() real Element of REAL

(k / 2) + (k / 2) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq - seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

k / 2 is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r + m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq - seq2) . n is Element of the U1 of X

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq - seq2) . m is Element of the U1 of X

dist (((seq - seq2) . n),((seq - seq2) . m)) is ext-real V31() real Element of REAL

seq2 . n is Element of the U1 of X

seq2 . m is Element of the U1 of X

dist ((seq2 . n),(seq2 . m)) is ext-real V31() real Element of REAL

seq . n is Element of the U1 of X

(seq . n) - (seq2 . n) is Element of the U1 of X

dist (((seq . n) - (seq2 . n)),((seq - seq2) . m)) is ext-real V31() real Element of REAL

seq . m is Element of the U1 of X

(seq . m) - (seq2 . m) is Element of the U1 of X

dist (((seq . n) - (seq2 . n)),((seq . m) - (seq2 . m))) is ext-real V31() real Element of REAL

dist ((seq . n),(seq . m)) is ext-real V31() real Element of REAL

(dist ((seq . n),(seq . m))) + (dist ((seq2 . n),(seq2 . m))) is ext-real V31() real Element of REAL

(k / 2) + (k / 2) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is ext-real V31() real Element of REAL

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq * seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

abs seq is ext-real V31() real Element of REAL

0 / (abs seq) is ext-real V31() real Element of REAL

k is ext-real V31() real Element of REAL

k / (abs seq) is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

seq2 . n is Element of the U1 of X

dist ((seq2 . m),(seq2 . n)) is ext-real V31() real Element of REAL

(abs seq) * (k / (abs seq)) is ext-real V31() real Element of REAL

(abs seq) " is ext-real V31() real Element of REAL

((abs seq) ") * k is ext-real V31() real Element of REAL

(abs seq) * (((abs seq) ") * k) is ext-real V31() real Element of REAL

(abs seq) * ((abs seq) ") is ext-real V31() real Element of REAL

((abs seq) * ((abs seq) ")) * k is ext-real V31() real Element of REAL

1 * k is ext-real V31() real Element of REAL

seq * (seq2 . m) is Element of the U1 of X

seq * (seq2 . n) is Element of the U1 of X

dist ((seq * (seq2 . m)),(seq * (seq2 . n))) is ext-real V31() real Element of REAL

(seq * (seq2 . m)) - (seq * (seq2 . n)) is Element of the U1 of X

||.((seq * (seq2 . m)) - (seq * (seq2 . n))).|| is ext-real V31() real Element of REAL

(seq2 . m) - (seq2 . n) is Element of the U1 of X

seq * ((seq2 . m) - (seq2 . n)) is Element of the U1 of X

||.(seq * ((seq2 . m) - (seq2 . n))).|| is ext-real V31() real Element of REAL

||.((seq2 . m) - (seq2 . n)).|| is ext-real V31() real Element of REAL

(abs seq) * ||.((seq2 . m) - (seq2 . n)).|| is ext-real V31() real Element of REAL

(abs seq) * (dist ((seq2 . m),(seq2 . n))) is ext-real V31() real Element of REAL

(seq * seq2) . m is Element of the U1 of X

dist (((seq * seq2) . m),(seq * (seq2 . n))) is ext-real V31() real Element of REAL

(seq * seq2) . n is Element of the U1 of X

dist (((seq * seq2) . m),((seq * seq2) . n)) is ext-real V31() real Element of REAL

k is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

seq2 . n is Element of the U1 of X

dist ((seq2 . m),(seq2 . n)) is ext-real V31() real Element of REAL

seq * (seq2 . m) is Element of the U1 of X

seq * (seq2 . n) is Element of the U1 of X

dist ((seq * (seq2 . m)),(seq * (seq2 . n))) is ext-real V31() real Element of REAL

0. X is V63(X) Element of the U1 of X

0 * (seq2 . n) is Element of the U1 of X

dist (H

dist (H

(seq * seq2) . m is Element of the U1 of X

dist (((seq * seq2) . m),(seq * (seq2 . n))) is ext-real V31() real Element of REAL

(seq * seq2) . n is Element of the U1 of X

dist (((seq * seq2) . m),((seq * seq2) . n)) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

- seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

(- 1) * seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is Element of the U1 of X

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 + seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq2 + seq) . m is Element of the U1 of X

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq2 + seq) . n is Element of the U1 of X

dist (((seq2 + seq) . m),((seq2 + seq) . n)) is ext-real V31() real Element of REAL

seq2 . m is Element of the U1 of X

(seq2 . m) + seq is Element of the U1 of X

seq2 . n is Element of the U1 of X

(seq2 . n) + seq is Element of the U1 of X

dist (((seq2 . m) + seq),((seq2 . n) + seq)) is ext-real V31() real Element of REAL

dist ((seq2 . m),(seq2 . n)) is ext-real V31() real Element of REAL

dist (seq,seq) is ext-real V31() real Element of REAL

(dist ((seq2 . m),(seq2 . n))) + (dist (seq,seq)) is ext-real V31() real Element of REAL

(dist ((seq2 . m),(seq2 . n))) + 0 is ext-real V31() real Element of REAL

dist (((seq2 + seq) . m),((seq2 . n) + seq)) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is Element of the U1 of X

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 - seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

- seq is Element of the U1 of X

seq2 + (- seq) is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is Element of the U1 of X

k is ext-real V31() real Element of REAL

k / 2 is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m is Element of the U1 of X

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . n is Element of the U1 of X

dist ((seq . m),(seq . n)) is ext-real V31() real Element of REAL

dist ((seq . m),seq2) is ext-real V31() real Element of REAL

dist ((seq . n),seq2) is ext-real V31() real Element of REAL

dist (seq2,(seq . n)) is ext-real V31() real Element of REAL

(dist ((seq . m),seq2)) + (dist (seq2,(seq . n))) is ext-real V31() real Element of REAL

(k / 2) + (k / 2) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is ext-real V31() real Element of REAL

k is V11() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . r is Element of the U1 of X

dist ((seq . r),(seq . r)) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

seq . m is Element of the U1 of X

dist ((seq2 . m),(seq . m)) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

r is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

r is ext-real V31() real Element of REAL

r / 2 is ext-real V31() real Element of REAL

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m is Element of the U1 of X

k . m is Element of the U1 of X

dist ((seq . m),(k . m)) is ext-real V31() real Element of REAL

seq2 . m is Element of the U1 of X

dist ((seq2 . m),(k . m)) is ext-real V31() real Element of REAL

dist ((seq . m),(seq2 . m)) is ext-real V31() real Element of REAL

(dist ((seq . m),(seq2 . m))) + (dist ((seq2 . m),(k . m))) is ext-real V31() real Element of REAL

(r / 2) + (r / 2) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m is Element of the U1 of X

seq2 . m is Element of the U1 of X

(seq . m) - (seq2 . m) is Element of the U1 of X

||.((seq . m) - (seq2 . m)).|| is ext-real V31() real Element of REAL

dist ((seq . m),(seq2 . m)) is ext-real V31() real Element of REAL

k is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m is Element of the U1 of X

seq2 . m is Element of the U1 of X

dist ((seq . m),(seq2 . m)) is ext-real V31() real Element of REAL

(seq . m) - (seq2 . m) is Element of the U1 of X

||.((seq . m) - (seq2 . m)).|| is ext-real V31() real Element of REAL

k is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r is ext-real V31() real Element of REAL

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m is Element of the U1 of X

seq2 . m is Element of the U1 of X

dist ((seq . m),(seq2 . m)) is ext-real V31() real Element of REAL

dist ((seq . m),(seq . m)) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

k / 3 is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r + m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . n is Element of the U1 of X

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

dist ((seq2 . n),(seq2 . m)) is ext-real V31() real Element of REAL

seq . n is Element of the U1 of X

seq . m is Element of the U1 of X

dist ((seq . n),(seq . m)) is ext-real V31() real Element of REAL

dist ((seq2 . n),(seq . m)) is ext-real V31() real Element of REAL

dist ((seq2 . n),(seq . n)) is ext-real V31() real Element of REAL

(dist ((seq2 . n),(seq . n))) + (dist ((seq . n),(seq . m))) is ext-real V31() real Element of REAL

dist ((seq . n),(seq2 . n)) is ext-real V31() real Element of REAL

(k / 3) + (k / 3) is ext-real V31() real Element of REAL

dist ((seq . m),(seq2 . m)) is ext-real V31() real Element of REAL

(dist ((seq2 . n),(seq . m))) + (dist ((seq . m),(seq2 . m))) is ext-real V31() real Element of REAL

((k / 3) + (k / 3)) + (k / 3) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

k / 2 is ext-real V31() real Element of REAL

lim seq is Element of the U1 of X

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r + m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . n is Element of the U1 of X

seq2 . n is Element of the U1 of X

dist ((seq . n),(seq2 . n)) is ext-real V31() real Element of REAL

dist ((seq2 . n),(lim seq)) is ext-real V31() real Element of REAL

dist ((seq2 . n),(seq . n)) is ext-real V31() real Element of REAL

dist ((seq . n),(lim seq)) is ext-real V31() real Element of REAL

(dist ((seq2 . n),(seq . n))) + (dist ((seq . n),(lim seq))) is ext-real V31() real Element of REAL

(k / 2) + (k / 2) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is Element of the U1 of X

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

lim seq2 is Element of the U1 of X

k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

lim k is Element of the U1 of X

r is ext-real V31() real Element of REAL

r / 2 is ext-real V31() real Element of REAL

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m1 + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

k . m is Element of the U1 of X

dist ((seq2 . m),(k . m)) is ext-real V31() real Element of REAL

dist ((k . m),seq) is ext-real V31() real Element of REAL

dist ((k . m),(seq2 . m)) is ext-real V31() real Element of REAL

dist ((seq2 . m),seq) is ext-real V31() real Element of REAL

(dist ((k . m),(seq2 . m))) + (dist ((seq2 . m),seq)) is ext-real V31() real Element of REAL

(r / 2) + (r / 2) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq + seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

r is ext-real V31() real Element of REAL

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq + seq2) . m1 is Element of the U1 of X

||.((seq + seq2) . m1).|| is ext-real V31() real Element of REAL

seq . m1 is Element of the U1 of X

seq2 . m1 is Element of the U1 of X

(seq . m1) + (seq2 . m1) is Element of the U1 of X

||.((seq . m1) + (seq2 . m1)).|| is ext-real V31() real Element of REAL

||.(seq . m1).|| is ext-real V31() real Element of REAL

||.(seq2 . m1).|| is ext-real V31() real Element of REAL

||.(seq . m1).|| + ||.(seq2 . m1).|| is ext-real V31() real Element of REAL

r + k is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

- seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is ext-real V31() real Element of REAL

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(- seq) . k is Element of the U1 of X

||.((- seq) . k).|| is ext-real V31() real Element of REAL

seq . k is Element of the U1 of X

- (seq . k) is Element of the U1 of X

||.(- (seq . k)).|| is ext-real V31() real Element of REAL

||.(seq . k).|| is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq - seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

- seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq + (- seq2) is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is ext-real V31() real Element of REAL

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq * seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real V31() real Element of REAL

abs seq is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq * seq2) . r is Element of the U1 of X

||.((seq * seq2) . r).|| is ext-real V31() real Element of REAL

seq2 . r is Element of the U1 of X

seq * (seq2 . r) is Element of the U1 of X

||.(seq * (seq2 . r)).|| is ext-real V31() real Element of REAL

||.(seq2 . r).|| is ext-real V31() real Element of REAL

(abs seq) * ||.(seq2 . r).|| is ext-real V31() real Element of REAL

(abs seq) * k is ext-real V31() real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq * seq2) . r is Element of the U1 of X

||.((seq * seq2) . r).|| is ext-real V31() real Element of REAL

seq2 . r is Element of the U1 of X

0 * (seq2 . r) is Element of the U1 of X

||.(0 * (seq2 . r)).|| is ext-real V31() real Element of REAL

0. X is V63(X) Element of the U1 of X

||.H

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is Element of the U1 of X

0. X is V63(X) Element of the U1 of X

k is ext-real V31() real set

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m1 is Element of the U1 of X

||.(seq . m1).|| is ext-real V31() real Element of REAL

r is ext-real V31() real Element of REAL

||.seq2.|| is ext-real V31() real Element of REAL

k is ext-real V31() real set

r is ext-real V31() real Element of REAL

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m1 is Element of the U1 of X

||.(seq . m1).|| is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 + 1 is V11() ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real V31() real Element of REAL

seq . (seq2 + 1) is Element of the U1 of X

||.(seq . (seq2 + 1)).|| is ext-real V31() real Element of REAL

||.(seq . (seq2 + 1)).|| + 1 is ext-real V31() real Element of REAL

r is ext-real V31() real Element of REAL

0 + 0 is V11() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m1 is Element of the U1 of X

||.(seq . m1).|| is ext-real V31() real Element of REAL

||.(seq . m1).|| + 0 is ext-real V31() real Element of REAL

k + 1 is ext-real V31() real Element of REAL

r is ext-real V31() real Element of REAL

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m1 is Element of the U1 of X

||.(seq . m1).|| is ext-real V31() real Element of REAL

k + 0 is ext-real V31() real Element of REAL

r is ext-real V31() real Element of REAL

m1 is ext-real V31() real Element of REAL

seq . 0 is Element of the U1 of X

||.(seq . 0).|| is ext-real V31() real Element of REAL

||.(seq . 0).|| + 1 is ext-real V31() real Element of REAL

seq2 is ext-real V31() real Element of REAL

0 + 0 is V11() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . k is Element of the U1 of X

||.(seq . k).|| is ext-real V31() real Element of REAL

||.(seq . k).|| + 0 is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is Element of the U1 of X

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

||.seq2.|| is ext-real V31() real Element of REAL

||.seq2.|| + 1 is ext-real V31() real Element of REAL

r is ext-real V31() real Element of REAL

0 + 0 is V11() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m1 is Element of the U1 of X

(seq . m1) - seq2 is Element of the U1 of X

||.((seq . m1) - seq2).|| is ext-real V31() real Element of REAL

||.(seq . m1).|| is ext-real V31() real Element of REAL

||.(seq . m1).|| - ||.seq2.|| is ext-real V31() real Element of REAL

r is ext-real V31() real Element of REAL

m1 is ext-real V31() real Element of REAL

m1 is ext-real V31() real Element of REAL

m1 + r is ext-real V31() real Element of REAL

m is ext-real V31() real Element of REAL

0 + r is ext-real V31() real Element of REAL

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . n is Element of the U1 of X

||.(seq . n).|| is ext-real V31() real Element of REAL

m1 + 0 is ext-real V31() real Element of REAL

r is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r is ext-real V31() real Element of REAL

r + 1 is ext-real V31() real Element of REAL

m1 is ext-real V31() real Element of REAL

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . m is Element of the U1 of X

seq2 . m is Element of the U1 of X

dist ((seq . m),(seq2 . m)) is ext-real V31() real Element of REAL

(seq2 . m) - (seq . m) is Element of the U1 of X

||.((seq2 . m) - (seq . m)).|| is ext-real V31() real Element of REAL

||.(seq2 . m).|| is ext-real V31() real Element of REAL

||.(seq . m).|| is ext-real V31() real Element of REAL

||.(seq2 . m).|| - ||.(seq . m).|| is ext-real V31() real Element of REAL

||.(seq . m).|| + 1 is ext-real V31() real Element of REAL

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

||.(seq2 . m).|| is ext-real V31() real Element of REAL

m1 is ext-real V31() real Element of REAL

m is ext-real V31() real Element of REAL

m is ext-real V31() real Element of REAL

m + m1 is ext-real V31() real Element of REAL

n is ext-real V31() real Element of REAL

0 + m1 is ext-real V31() real Element of REAL

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

||.(seq2 . m).|| is ext-real V31() real Element of REAL

m + 0 is ext-real V31() real Element of REAL

m1 is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is V1() V4( NAT ) V5( NAT ) V6() V11() V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))

seq * k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

r is ext-real V31() real Element of REAL

m1 is ext-real V31() real Element of REAL

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

k . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . (k . m) is Element of the U1 of X

||.(seq2 . m).|| is ext-real V31() real Element of REAL

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

||.(seq2 . m).|| is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is Element of the U1 of X

r is V1() V4( NAT ) V5( NAT ) V6() V11() V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))

seq * r is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

m1 is ext-real V31() real Element of REAL

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . m is Element of the U1 of X

seq . (r . m) is Element of the U1 of X

(seq2 . m) - k is Element of the U1 of X

||.((seq2 . m) - k).|| is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

lim seq is Element of the U1 of X

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

lim seq2 is Element of the U1 of X

k is V1() V4( NAT ) V5( NAT ) V6() V11() V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))

seq2 * k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq2

r is ext-real V31() real Element of REAL

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k . n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . n is Element of the U1 of X

seq2 . (k . n) is Element of the U1 of X

dist ((seq . n),(lim seq2)) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is V1() V4( NAT ) V5( NAT ) V6() V11() V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))

seq * k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

r is ext-real V31() real Element of REAL

m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k . n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq2 . n is Element of the U1 of X

seq . (k . n) is Element of the U1 of X

seq2 . m is Element of the U1 of X

seq . (k . m) is Element of the U1 of X

dist ((seq2 . n),(seq2 . m)) is ext-real V31() real Element of REAL

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq ^\ seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq ^\ seq2) ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq ^\ seq2

seq ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

(seq ^\ k) ^\ seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq ^\ k

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

((seq ^\ seq2) ^\ k) . r is Element of the U1 of X

r + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq ^\ seq2) . (r + k) is Element of the U1 of X

(r + k) + seq2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . ((r + k) + seq2) is Element of the U1 of X

r + seq2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(r + seq2) + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . ((r + seq2) + k) is Element of the U1 of X

(seq ^\ k) . (r + seq2) is Element of the U1 of X

((seq ^\ k) ^\ seq2) . r is Element of the U1 of X

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq ^\ seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq ^\ seq2) ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq ^\ seq2

seq2 + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq ^\ (seq2 + k) is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

((seq ^\ seq2) ^\ k) . r is Element of the U1 of X

r + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq ^\ seq2) . (r + k) is Element of the U1 of X

(r + k) + seq2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . ((r + k) + seq2) is Element of the U1 of X

r + (seq2 + k) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

seq . (r + (seq2 + k)) is Element of the U1 of X

(seq ^\ (seq2 + k)) . r is Element of the U1 of X

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq + seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq + seq2) ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq + seq2

seq ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

seq2 ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq2

(seq ^\ k) + (seq2 ^\ k) is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

((seq + seq2) ^\ k) . r is Element of the U1 of X

r + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq + seq2) . (r + k) is Element of the U1 of X

seq . (r + k) is Element of the U1 of X

seq2 . (r + k) is Element of the U1 of X

(seq . (r + k)) + (seq2 . (r + k)) is Element of the U1 of X

(seq ^\ k) . r is Element of the U1 of X

((seq ^\ k) . r) + (seq2 . (r + k)) is Element of the U1 of X

(seq2 ^\ k) . r is Element of the U1 of X

((seq ^\ k) . r) + ((seq2 ^\ k) . r) is Element of the U1 of X

((seq ^\ k) + (seq2 ^\ k)) . r is Element of the U1 of X

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

- seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(- seq) ^\ seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of - seq

seq ^\ seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

- (seq ^\ seq2) is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

((- seq) ^\ seq2) . k is Element of the U1 of X

k + seq2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(- seq) . (k + seq2) is Element of the U1 of X

seq . (k + seq2) is Element of the U1 of X

- (seq . (k + seq2)) is Element of the U1 of X

(seq ^\ seq2) . k is Element of the U1 of X

- ((seq ^\ seq2) . k) is Element of the U1 of X

(- (seq ^\ seq2)) . k is Element of the U1 of X

X is V56() V82() V107() V108() V109() V110() V111() V112() V113() RealUnitarySpace-like UNITSTR

the U1 of X is V11() set

K20(NAT, the U1 of X) is set

K19(K20(NAT, the U1 of X)) is set

seq is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

seq - seq2 is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) Element of K19(K20(NAT, the U1 of X))

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(seq - seq2) ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq - seq2

seq ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq

seq2 ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq2

(seq ^\ k) - (seq2 ^\ k) is V1() V4( NAT ) V5( the