:: 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₁(X),(0 * (seq2 . n))) is ext-real V31() real Element of REAL
dist (H₁(X),H₁(X)) 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
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 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
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 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))
(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 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))
- (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))
(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))
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 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 V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of seq2
seq * (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
seq2 . (r + k) is Element of the U1 of X
seq * (seq2 . (r + k)) is Element of the U1 of X
(seq2 ^\ k) . r is Element of the U1 of X
seq * ((seq2 ^\ k) . r) 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 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
lim (seq ^\ seq2) is Element of the U1 of X
lim seq 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))
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 ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of 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
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 Element of the U1 of X
m is ext-real V31() real Element of REAL
m1 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
n + 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
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 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 set
(n + k) + 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
m1 - k is ext-real V31() real Element of REAL
l2 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 + l2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT
m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT
m2 + 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 . m2 is Element of the U1 of X
(seq . m2) - m1 is Element of the U1 of X
||.((seq . m2) - m1).|| is ext-real V31() real Element of REAL
seq2 . m1 is Element of the U1 of X
(seq2 . m1) - m1 is Element of the U1 of X
||.((seq2 . m1) - m1).|| is ext-real V31() real Element of REAL
m1 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))
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 ^\ k is V1() V4( NAT ) V5( the U1 of X) V6() V11() V14( NAT ) V18( NAT , the U1 of X) subsequence of 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
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
m1 + 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
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
m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real set
(m1 + k) + 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
n - k 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
m1 + 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
l2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT
m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real set
(m1 + k) + m2 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 - k is ext-real V31() real Element of REAL
m2 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 + m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT
l3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V31() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT
l2 + 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
l3 + 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 . l2 is Element of the U1 of X
seq . l3 is Element of the U1 of X
dist ((seq . l2),(seq . l3)) is ext-real V31() real Element of REAL
dist ((seq2 . n),(seq . l3)) 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
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
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
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
(seq ^\ k) . n is Element of the U1 of X
(seq2 ^\ k) . n is Element of the U1 of X
dist (((seq ^\ k) . n),((seq2 ^\ k) . n)) is ext-real V31() real Element of REAL
n + 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 . (n + k) is Element of the U1 of X
seq2 . (n + k) is Element of the U1 of X
dist ((seq . (n + k)),(seq2 . (n + k))) is ext-real V31() real Element of REAL
dist (((seq ^\ k) . n),(seq2 . (n + 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 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
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
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))