:: TOPREAL9 semantic presentation

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)

{ b

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

{ b

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

{ b

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

{ 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)

- 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

{ 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)

- 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

{ 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)

- 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

{ 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)

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

{ 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)

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