REAL is V179() V180() V181() V185() set
NAT is V179() V180() V181() V182() V183() V184() V185() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V179() V185() set
RAT is V179() V180() V181() V182() V185() set
INT is V179() V180() V181() V182() V183() V185() set
K7(COMPLEX,COMPLEX) is V16() complex-yielding set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V16() complex-yielding set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is V16() complex-yielding ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is V16() complex-yielding ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V16() V20( RAT ) complex-yielding ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V16() V20( RAT ) complex-yielding ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V16() V20( RAT ) V20( INT ) complex-yielding ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V16() V20( RAT ) V20( INT ) complex-yielding ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V16() V20( RAT ) V20( INT ) complex-yielding ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V16() V20( RAT ) V20( INT ) complex-yielding ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
omega is V179() V180() V181() V182() V183() V184() V185() set
K6(omega) is set
K6(NAT) is set
K343() is TopStruct
the carrier of K343() is set
1 is non empty ordinal natural V11() real ext-real positive non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
K7(1,1) is V16() V20( RAT ) V20( INT ) complex-yielding ext-real-valued real-valued natural-valued set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V16() V20( RAT ) V20( INT ) complex-yielding ext-real-valued real-valued natural-valued set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V16() complex-yielding ext-real-valued real-valued set
K6(K7(K7(1,1),REAL)) is set
2 is non empty ordinal natural V11() real ext-real positive non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
K7(2,2) is V16() V20( RAT ) V20( INT ) complex-yielding ext-real-valued real-valued natural-valued set
K7(K7(2,2),REAL) is V16() complex-yielding ext-real-valued real-valued set
K6(K7(K7(2,2),REAL)) is set
K514() is non empty V128() L10()
the carrier of K514() is non empty set
K519() is non empty V128() V150() V151() V152() V154() V201() V202() V203() V204() V205() V206() L10()
K520() is non empty V128() V152() V154() V204() V205() V206() M19(K519())
K521() is non empty V128() V150() V152() V154() V204() V205() V206() V207() M22(K519(),K520())
K523() is non empty V128() V150() V152() V154() L10()
K524() is non empty V128() V150() V152() V154() V207() M19(K523())
TOP-REAL 2 is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
NonZero (TOP-REAL 2) is Element of K6( the carrier of (TOP-REAL 2))
K6( the carrier of (TOP-REAL 2)) is set
[#] (TOP-REAL 2) is non empty non proper non proper closed closed convex Element of K6( the carrier of (TOP-REAL 2))
0. (TOP-REAL 2) is V16() V19( NAT ) V21() V37() V44(2) FinSequence-like FinSubsequence-like V69( TOP-REAL 2) complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is V16() V19( NAT ) V21() V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
{(0. (TOP-REAL 2))} is non empty V24() set
([#] (TOP-REAL 2)) \ {(0. (TOP-REAL 2))} is Element of K6( the carrier of (TOP-REAL 2))
K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))) is V16() set
K6(K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)))) is set
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is V16() set
K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2))) is set
{} is empty V16() non-zero V18() V19( NAT ) V20( RAT ) V21() V22() constant V24() V37() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V179() V180() V181() V182() V183() V184() V185() set
the empty V16() non-zero V18() V19( NAT ) V20( RAT ) V21() V22() constant V24() V37() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V179() V180() V181() V182() V183() V184() V185() set is empty V16() non-zero V18() V19( NAT ) V20( RAT ) V21() V22() constant V24() V37() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V179() V180() V181() V182() V183() V184() V185() set
{{},1} is non empty set
3 is non empty ordinal natural V11() real ext-real positive non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
0 is empty ordinal natural V11() real ext-real non positive non negative V16() non-zero V18() V19( NAT ) V20( RAT ) V21() V22() constant V24() V33() V34() V37() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V179() V180() V181() V182() V183() V184() V185() Element of NAT
sqrt 0 is V11() real ext-real Element of REAL
4 is non empty ordinal natural V11() real ext-real positive non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
a is ordinal natural V11() real ext-real non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),b,r) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),b,w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
b - b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * b is V16() V21() set
K382((TOP-REAL a),b,(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),b,(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + (- b) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
b - b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(b) is V16() V21() complex-yielding set
K419(b,K448(b)) is V16() V21() set
(b - b) + r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(b - b),r) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(b - b) + r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(b + w) - b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K382((TOP-REAL a),(b + w),(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(b + w),(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(b + w) + (- b) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(b + w) - b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K419((b + w),K448(b)) is V16() V21() set
0. (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like V69( TOP-REAL a) complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the ZeroF of (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(b - b) + w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(b - b),w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(b - b) + w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(0. (TOP-REAL a)) + w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(0. (TOP-REAL a)),w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(0. (TOP-REAL a)) + w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
a is ordinal natural V11() real ext-real non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
1.REAL a is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
1* a is V16() V19( NAT ) V20( REAL ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL a
REAL a is non empty V24() FinSequence-membered FinSequenceSet of REAL
a -tuples_on REAL is V24() FinSequence-membered FinSequenceSet of REAL
a |-> 1 is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of a -tuples_on REAL
b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + (1.REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),b,(1.REAL a)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + (1.REAL a) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
0.REAL a is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
a |-> 0 is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of a -tuples_on REAL
0. (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like V69( TOP-REAL a) complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the ZeroF of (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + (0. (TOP-REAL a)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),b,(0. (TOP-REAL a))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b + (0. (TOP-REAL a)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
a is ordinal natural V11() real ext-real non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
b is V11() real ext-real set
1 - b is V11() real ext-real Element of REAL
- b is V11() real ext-real set
1 + (- b) is V11() real ext-real set
r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(1 - b) * r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(1 - b) * r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b * w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b * w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) + (b * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),((1 - b) * r),(b * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) * r) + (b * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
s is set
0. (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like V69( TOP-REAL a) complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the ZeroF of (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(((1 - b) * r) + (b * w)) - r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * r is V16() V21() set
K382((TOP-REAL a),(((1 - b) * r) + (b * w)),(- r)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(((1 - b) * r) + (b * w)),(- r)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(((1 - b) * r) + (b * w)) + (- r) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(((1 - b) * r) + (b * w)) - r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(r) is V16() V21() complex-yielding set
K419((((1 - b) * r) + (b * w)),K448(r)) is V16() V21() set
((1 - b) * r) - r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K382((TOP-REAL a),((1 - b) * r),(- r)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),((1 - b) * r),(- r)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) * r) + (- r) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) - r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K419(((1 - b) * r),K448(r)) is V16() V21() set
(((1 - b) * r) - r) + (b * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(((1 - b) * r) - r),(b * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(((1 - b) * r) - r) + (b * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
1 * r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
1 * r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) - (1 * r) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- (1 * r) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- (1 * r) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(- 1) * (1 * r) is V16() V21() set
K382((TOP-REAL a),((1 - b) * r),(- (1 * r))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),((1 - b) * r),(- (1 * r))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) * r) + (- (1 * r)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) - (1 * r) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448((1 * r)) is V16() V21() complex-yielding set
K419(((1 - b) * r),K448((1 * r))) is V16() V21() set
(((1 - b) * r) - (1 * r)) + (b * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(((1 - b) * r) - (1 * r)),(b * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(((1 - b) * r) - (1 * r)) + (b * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(1 - b) - 1 is V11() real ext-real Element of REAL
(1 - b) + (- 1) is V11() real ext-real set
((1 - b) - 1) * r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) - 1) * r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(((1 - b) - 1) * r) + (b * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(((1 - b) - 1) * r),(b * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(((1 - b) - 1) * r) + (b * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
b * r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b * r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(b * w) - (b * r) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- (b * r) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- (b * r) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(- 1) * (b * r) is V16() V21() set
K382((TOP-REAL a),(b * w),(- (b * r))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(b * w),(- (b * r))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(b * w) + (- (b * r)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(b * w) - (b * r) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448((b * r)) is V16() V21() complex-yielding set
K419((b * w),K448((b * r))) is V16() V21() set
w - r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K382((TOP-REAL a),w,(- r)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),w,(- r)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
w + (- r) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
w - r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K419(w,K448(r)) is V16() V21() set
b * (w - r) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b * (w - r) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
0 * w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
0 * w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r + (0 * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),r,(0 * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
r + (0 * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r + (0. (TOP-REAL a)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),r,(0. (TOP-REAL a))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
r + (0. (TOP-REAL a)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(1 - b) + b is V11() real ext-real Element of REAL
((1 - b) + b) * r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) + b) * r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(((1 - b) * r) + (b * w)) - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(- 1) * w is V16() V21() set
K382((TOP-REAL a),(((1 - b) * r) + (b * w)),(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(((1 - b) * r) + (b * w)),(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(((1 - b) * r) + (b * w)) + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(((1 - b) * r) + (b * w)) - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(w) is V16() V21() complex-yielding set
K419((((1 - b) * r) + (b * w)),K448(w)) is V16() V21() set
(b * w) - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K382((TOP-REAL a),(b * w),(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(b * w),(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(b * w) + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(b * w) - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K419((b * w),K448(w)) is V16() V21() set
((1 - b) * r) + ((b * w) - w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),((1 - b) * r),((b * w) - w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) * r) + ((b * w) - w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive Element of REAL
(- 1) * w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(- 1) * w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(b * w) + ((- 1) * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(b * w),((- 1) * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(b * w) + ((- 1) * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) + ((b * w) + ((- 1) * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),((1 - b) * r),((b * w) + ((- 1) * w))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) * r) + ((b * w) + ((- 1) * w)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(- 1) + b is V11() real ext-real Element of REAL
((- 1) + b) * w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((- 1) + b) * w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) + (((- 1) + b) * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),((1 - b) * r),(((- 1) + b) * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) * r) + (((- 1) + b) * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- (1 - b) is V11() real ext-real Element of REAL
(- (1 - b)) * w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(- (1 - b)) * w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) + ((- (1 - b)) * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),((1 - b) * r),((- (1 - b)) * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) * r) + ((- (1 - b)) * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(1 - b) * w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(1 - b) * w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) - ((1 - b) * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- ((1 - b) * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- ((1 - b) * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(- 1) * ((1 - b) * w) is V16() V21() set
K382((TOP-REAL a),((1 - b) * r),(- ((1 - b) * w))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),((1 - b) * r),(- ((1 - b) * w))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) * r) + (- ((1 - b) * w)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) * r) - ((1 - b) * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(((1 - b) * w)) is V16() V21() complex-yielding set
K419(((1 - b) * r),K448(((1 - b) * w))) is V16() V21() set
r - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K382((TOP-REAL a),r,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),r,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
r + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K419(r,K448(w)) is V16() V21() set
(1 - b) * (r - w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(1 - b) * (r - w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(1 - b) + b is V11() real ext-real Element of REAL
0 + b is V11() real ext-real Element of REAL
1 * w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
1 * w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(0. (TOP-REAL a)) + (1 * w) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),(0. (TOP-REAL a)),(1 * w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(0. (TOP-REAL a)) + (1 * w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - b) + b) * w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
((1 - b) + b) * w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
a is V16() V19( NAT ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set
|.a.| is V11() real ext-real non negative Element of REAL
sqr a is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt (a,a) is V16() V21() set
Sum (sqr a) is V11() real ext-real Element of REAL
sqrt (Sum (sqr a)) is V11() real ext-real Element of REAL
|.a.| ^2 is V11() real ext-real Element of REAL
|.a.| * |.a.| is V11() real ext-real non negative set
a is V11() real ext-real set
b is non empty Reflexive discerning V103() triangle MetrStruct
the carrier of b is non empty set
r is Element of the carrier of b
w is Element of the carrier of b
s is Element of the carrier of b
cl_Ball (s,a) is Element of K6( the carrier of b)
K6( the carrier of b) is set
{s} is non empty set
a is ordinal natural V11() real ext-real non negative set
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
r is V11() real ext-real set
b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
{ b1 where b1 is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a) : not r <= |.(b1 - b).| } is set
K6( the carrier of (TOP-REAL a)) is set
w is set
s is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s - b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * b is V16() V21() set
K382((TOP-REAL a),s,(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),s,(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s + (- b) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
s - b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(b) is V16() V21() complex-yielding set
K419(s,K448(b)) is V16() V21() set
|.(s - b).| is V11() real ext-real non negative Element of REAL
sqr (s - b) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((s - b),(s - b)) is V16() V21() set
Sum (sqr (s - b)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (s - b))) is V11() real ext-real Element of REAL
{ b1 where b1 is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a) : |.(b1 - b).| <= r } is set
w is set
s is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s - b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * b is V16() V21() set
K382((TOP-REAL a),s,(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),s,(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s + (- b) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
s - b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(b) is V16() V21() complex-yielding set
K419(s,K448(b)) is V16() V21() set
|.(s - b).| is V11() real ext-real non negative Element of REAL
sqr (s - b) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((s - b),(s - b)) is V16() V21() set
Sum (sqr (s - b)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (s - b))) is V11() real ext-real Element of REAL
{ b1 where b1 is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a) : |.(b1 - b).| = r } is set
w is set
s is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s - b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- b is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * b is V16() V21() set
K382((TOP-REAL a),s,(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),s,(- b)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s + (- b) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
s - b is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(b) is V16() V21() complex-yielding set
K419(s,K448(b)) is V16() V21() set
|.(s - b).| is V11() real ext-real non negative Element of REAL
sqr (s - b) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((s - b),(s - b)) is V16() V21() set
Sum (sqr (s - b)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (s - b))) is V11() real ext-real Element of REAL
a is ordinal natural V11() real ext-real non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
b is V11() real ext-real set
r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(a,w,b) is Element of K6( the carrier of (TOP-REAL a))
K6( the carrier of (TOP-REAL a)) is set
{ b1 where b1 is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a) : not b <= |.(b1 - w).| } is set
r - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * w is V16() V21() set
K382((TOP-REAL a),r,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),r,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
r + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(w) is V16() V21() complex-yielding set
K419(r,K448(w)) is V16() V21() set
|.(r - w).| is V11() real ext-real non negative Element of REAL
sqr (r - w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((r - w),(r - w)) is V16() V21() set
Sum (sqr (r - w)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (r - w))) is V11() real ext-real Element of REAL
s is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K382((TOP-REAL a),s,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),s,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
s - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K419(s,K448(w)) is V16() V21() set
|.(s - w).| is V11() real ext-real non negative Element of REAL
sqr (s - w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((s - w),(s - w)) is V16() V21() set
Sum (sqr (s - w)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (s - w))) is V11() real ext-real Element of REAL
a is ordinal natural V11() real ext-real non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
b is V11() real ext-real set
r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(a,w,b) is Element of K6( the carrier of (TOP-REAL a))
K6( the carrier of (TOP-REAL a)) is set
{ b1 where b1 is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a) : |.(b1 - w).| <= b } is set
r - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * w is V16() V21() set
K382((TOP-REAL a),r,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),r,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
r + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(w) is V16() V21() complex-yielding set
K419(r,K448(w)) is V16() V21() set
|.(r - w).| is V11() real ext-real non negative Element of REAL
sqr (r - w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((r - w),(r - w)) is V16() V21() set
Sum (sqr (r - w)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (r - w))) is V11() real ext-real Element of REAL
s is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K382((TOP-REAL a),s,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),s,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
s - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K419(s,K448(w)) is V16() V21() set
|.(s - w).| is V11() real ext-real non negative Element of REAL
sqr (s - w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((s - w),(s - w)) is V16() V21() set
Sum (sqr (s - w)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (s - w))) is V11() real ext-real Element of REAL
a is ordinal natural V11() real ext-real non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
b is V11() real ext-real set
r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
(a,w,b) is Element of K6( the carrier of (TOP-REAL a))
K6( the carrier of (TOP-REAL a)) is set
{ b1 where b1 is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a) : |.(b1 - w).| = b } is set
r - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * w is V16() V21() set
K382((TOP-REAL a),r,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),r,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
r + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448(w) is V16() V21() complex-yielding set
K419(r,K448(w)) is V16() V21() set
|.(r - w).| is V11() real ext-real non negative Element of REAL
sqr (r - w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((r - w),(r - w)) is V16() V21() set
Sum (sqr (r - w)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (r - w))) is V11() real ext-real Element of REAL
s is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s - w is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K382((TOP-REAL a),s,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),s,(- w)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
s + (- w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
s - w is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K419(s,K448(w)) is V16() V21() set
|.(s - w).| is V11() real ext-real non negative Element of REAL
sqr (s - w) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((s - w),(s - w)) is V16() V21() set
Sum (sqr (s - w)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (s - w))) is V11() real ext-real Element of REAL
a is ordinal natural V11() real ext-real non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
0. (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like V69( TOP-REAL a) complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the ZeroF of (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b is V11() real ext-real set
(a,(0. (TOP-REAL a)),b) is Element of K6( the carrier of (TOP-REAL a))
K6( the carrier of (TOP-REAL a)) is set
{ b1 where b1 is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a) : not b <= |.(b1 - (0. (TOP-REAL a))).| } is set
r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
|.r.| is V11() real ext-real non negative Element of REAL
sqr r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt (r,r) is V16() V21() set
Sum (sqr r) is V11() real ext-real Element of REAL
sqrt (Sum (sqr r)) is V11() real ext-real Element of REAL
r - (0. (TOP-REAL a)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- (0. (TOP-REAL a)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- (0. (TOP-REAL a)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * (0. (TOP-REAL a)) is V16() V21() set
K382((TOP-REAL a),r,(- (0. (TOP-REAL a)))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)))
K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)) is V16() set
K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) is V16() set
K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a))) is set
K350( the carrier of (TOP-REAL a), the U7 of (TOP-REAL a),r,(- (0. (TOP-REAL a)))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
r + (- (0. (TOP-REAL a))) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r - (0. (TOP-REAL a)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
K448((0. (TOP-REAL a))) is V16() V21() complex-yielding set
K419(r,K448((0. (TOP-REAL a)))) is V16() V21() set
|.(r - (0. (TOP-REAL a))).| is V11() real ext-real non negative Element of REAL
sqr (r - (0. (TOP-REAL a))) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt ((r - (0. (TOP-REAL a))),(r - (0. (TOP-REAL a)))) is V16() V21() set
Sum (sqr (r - (0. (TOP-REAL a)))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (r - (0. (TOP-REAL a))))) is V11() real ext-real Element of REAL
a is ordinal natural V11() real ext-real non negative V33() V34() V179() V180() V181() V182() V183() V184() Element of NAT
TOP-REAL a is non empty TopSpace-like V126() V191() V192() V209() V210() V211() V212() V213() V214() V215() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL a) is non empty set
0. (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like V69( TOP-REAL a) complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the ZeroF of (TOP-REAL a) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
b is V11() real ext-real set
(a,(0. (TOP-REAL a)),b) is Element of K6( the carrier of (TOP-REAL a))
K6( the carrier of (TOP-REAL a)) is set
{ b1 where b1 is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a) : |.(b1 - (0. (TOP-REAL a))).| <= b } is set
r is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
|.r.| is V11() real ext-real non negative Element of REAL
sqr r is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
mlt (r,r) is V16() V21() set
Sum (sqr r) is V11() real ext-real Element of REAL
sqrt (Sum (sqr r)) is V11() real ext-real Element of REAL
r - (0. (TOP-REAL a)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- (0. (TOP-REAL a)) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
- (0. (TOP-REAL a)) is V16() V19( NAT ) V20( REAL ) V21() V37() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- 1 is V11() real ext-real non positive set
(- 1) * (0. (TOP-REAL a)) is V16() V21() set
K382((TOP-REAL a),r,(- (0. (TOP-REAL a)))) is V16() V19( NAT ) V21() V37() V44(a) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the U7 of (TOP-REAL a) is V16() V21() V30(K7( the carrier of (TOP-REAL a), the carrier of (TOP-REAL a)), the carrier of (TOP-REAL a)) Element of K6(K7(K7( the carrier of (TOP-REAL a), the carrier of (