:: EUCLID_2 semantic presentation

REAL is V1() V37() V129() V130() V131() V135() set
NAT is V129() V130() V131() V132() V133() V134() V135() M2(K6(REAL))
K6(REAL) is set
COMPLEX is V1() V37() V129() V135() set
RAT is V1() V37() V129() V130() V131() V132() V135() set
INT is V1() V37() V129() V130() V131() V132() V133() V135() set
K7(COMPLEX,COMPLEX) is complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
omega is V129() V130() V131() V132() V133() V134() V135() set
K6(omega) is set
K6(NAT) is set
K391() is V50() V78() L8()
the U1 of K391() is set
K396() is V50() V78() V100() V101() V102() V104() V151() V152() V153() V154() V155() V156() L8()
K397() is V50() V78() V102() V104() V154() V155() V156() M13(K396())
K398() is V50() V78() V100() V102() V104() V154() V155() V156() V157() M16(K396(),K397())
K400() is V50() V78() V100() V102() V104() L8()
K401() is V50() V78() V100() V102() V104() V157() M13(K400())
1 is V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
K7(1,1) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(1,1),REAL)) is set
2 is V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
K7(2,2) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(2,2),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL 2) is set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
0 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
3 is V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
sqrt 0 is V11() real ext-real M2( REAL )
4 is V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
0 is set
n is natural V11() real ext-real set
n -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
REAL * is V1() functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
0* n is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
REAL n is V1() functional FinSequence-membered FinSequenceSet of REAL
p is natural V11() real ext-real set
p is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
mlt (p,(0* n)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,(0* n)) is set
(mlt (p,(0* n))) . p is V11() real ext-real set
n |-> 0 is V16() empty-yielding V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like set
Seg n is V37() V44(n) V129() V130() V131() V132() V133() V134() M2(K6(NAT))
K207((Seg n),0) is V16() V19( Seg n) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg n,{0}) V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued M2(K6(K7((Seg n),{0})))
{0} is V129() V130() V131() V132() V133() V134() set
K7((Seg n),{0}) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg n),{0})) is set
(0* n) . p is V11() real ext-real set
dom (0* n) is V129() V130() V131() V132() V133() V134() M2(K6(NAT))
p . p is V11() real ext-real set
(p . p) * ((0* n) . p) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
n -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
REAL * is V1() functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
0* n is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
REAL n is V1() functional FinSequence-membered FinSequenceSet of REAL
p is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
mlt (p,(0* n)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,(0* n)) is set
len (0* n) is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
dom (0* n) is V129() V130() V131() V132() V133() V134() M2(K6(NAT))
q is natural V11() real ext-real set
(mlt (p,(0* n))) . q is V11() real ext-real set
(0* n) . q is V11() real ext-real set
n |-> 0 is V16() empty-yielding V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
Seg n is V37() V44(n) V129() V130() V131() V132() V133() V134() M2(K6(NAT))
K207((Seg n),0) is V16() V19( Seg n) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg n,{0}) V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued M2(K6(K7((Seg n),{0})))
{0} is V129() V130() V131() V132() V133() V134() set
K7((Seg n),{0}) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg n),{0})) is set
(n |-> 0) . q is V1() V11() real ext-real Function-like functional FinSequence-membered V129() V130() V131() V132() V133() V134() V135() set
p is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K167(),p,p) is set
len (mlt (p,p)) is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
dom (mlt (p,(0* n))) is V129() V130() V131() V132() V133() V134() M2(K6(NAT))
1 / 4 is V11() real ext-real V34() M2( RAT )
n is natural V11() real ext-real set
REAL n is V1() functional FinSequence-membered FinSequenceSet of REAL
p is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
p is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
q is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
q + q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),q,q2) is set
|.(q + q2).| is V11() real ext-real non negative M2( REAL )
|.(q + q2).| ^2 is V11() real ext-real M2( REAL )
K37(|.(q + q2).|,|.(q + q2).|) is V11() real ext-real non negative set
q - q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),q,q2) is set
K325(q2) is V16() Function-like complex-valued set
K163() * q2 is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * q2 is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * q2 is V16() Function-like complex-valued ext-real-valued real-valued set
K296(q,K325(q2)) is V16() Function-like set
|.(q - q2).| is V11() real ext-real non negative M2( REAL )
|.(q - q2).| ^2 is V11() real ext-real M2( REAL )
K37(|.(q - q2).|,|.(q - q2).|) is V11() real ext-real non negative set
(|.(q + q2).| ^2) - (|.(q - q2).| ^2) is V11() real ext-real M2( REAL )
(1 / 4) * ((|.(q + q2).| ^2) - (|.(q - q2).| ^2)) is V11() real ext-real M2( REAL )
n -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
REAL * is V1() functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
sqr (q + q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
sqrreal is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
sqrreal * (q + q2) is V16() Function-like complex-valued ext-real-valued real-valued set
mlt ((q + q2),(q + q2)) is V16() Function-like set
K203(K167(),(q + q2),(q + q2)) is set
sqr (q - q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
sqrreal * (q - q2) is V16() Function-like complex-valued ext-real-valued real-valued set
mlt ((q - q2),(q - q2)) is V16() Function-like set
K203(K167(),(q - q2),(q - q2)) is set
Sum (sqr (q + q2)) is V11() real ext-real M2( REAL )
sqrt (Sum (sqr (q + q2))) is V11() real ext-real M2( REAL )
(sqrt (Sum (sqr (q + q2)))) ^2 is V11() real ext-real M2( REAL )
K37((sqrt (Sum (sqr (q + q2)))),(sqrt (Sum (sqr (q + q2))))) is V11() real ext-real set
((sqrt (Sum (sqr (q + q2)))) ^2) - (|.(q - q2).| ^2) is V11() real ext-real M2( REAL )
(1 / 4) * (((sqrt (Sum (sqr (q + q2)))) ^2) - (|.(q - q2).| ^2)) is V11() real ext-real M2( REAL )
Sum (sqr (q - q2)) is V11() real ext-real M2( REAL )
sqrt (Sum (sqr (q - q2))) is V11() real ext-real M2( REAL )
(sqrt (Sum (sqr (q - q2)))) ^2 is V11() real ext-real M2( REAL )
K37((sqrt (Sum (sqr (q - q2)))),(sqrt (Sum (sqr (q - q2))))) is V11() real ext-real set
((sqrt (Sum (sqr (q + q2)))) ^2) - ((sqrt (Sum (sqr (q - q2)))) ^2) is V11() real ext-real M2( REAL )
(1 / 4) * (((sqrt (Sum (sqr (q + q2)))) ^2) - ((sqrt (Sum (sqr (q - q2)))) ^2)) is V11() real ext-real M2( REAL )
(Sum (sqr (q + q2))) - (Sum (sqr (q - q2))) is V11() real ext-real M2( REAL )
(sqr (q + q2)) - (sqr (q - q2)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(sqr (q + q2)),(sqr (q - q2))) is set
K325((sqr (q - q2))) is V16() Function-like complex-valued set
K163() * (sqr (q - q2)) is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * (sqr (q - q2)) is V16() Function-like set
K369(K38(1)) * (sqr (q - q2)) is V16() Function-like complex-valued ext-real-valued real-valued set
K296((sqr (q + q2)),K325((sqr (q - q2)))) is V16() Function-like set
Sum ((sqr (q + q2)) - (sqr (q - q2))) is V11() real ext-real M2( REAL )
p3 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
q1 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
mlt (p3,q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K167(),p3,q1) is set
2 * (mlt (p3,q1)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K369(2) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),2,K83(REAL)) is set
K369(2) * (mlt (p3,q1)) is V16() Function-like complex-valued ext-real-valued real-valued set
sqr q1 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
sqrreal * q1 is V16() Function-like complex-valued ext-real-valued real-valued set
mlt (q1,q1) is V16() Function-like set
K203(K167(),q1,q1) is set
(2 * (mlt (p3,q1))) + (sqr q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),(2 * (mlt (p3,q1))),(sqr q1)) is set
((2 * (mlt (p3,q1))) + (sqr q1)) + (2 * (mlt (p3,q1))) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),((2 * (mlt (p3,q1))) + (sqr q1)),(2 * (mlt (p3,q1)))) is set
(2 * (mlt (p3,q1))) + ((2 * (mlt (p3,q1))) + (sqr q1)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),(2 * (mlt (p3,q1))),((2 * (mlt (p3,q1))) + (sqr q1))) is set
(2 * (mlt (p3,q1))) + (2 * (mlt (p3,q1))) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),(2 * (mlt (p3,q1))),(2 * (mlt (p3,q1)))) is set
((2 * (mlt (p3,q1))) + (2 * (mlt (p3,q1)))) + (sqr q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),((2 * (mlt (p3,q1))) + (2 * (mlt (p3,q1)))),(sqr q1)) is set
sqr p3 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
sqrreal * p3 is V16() Function-like complex-valued ext-real-valued real-valued set
mlt (p3,p3) is V16() Function-like set
K203(K167(),p3,p3) is set
(sqr p3) + ((2 * (mlt (p3,q1))) + (sqr q1)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),(sqr p3),((2 * (mlt (p3,q1))) + (sqr q1))) is set
((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),((2 * (mlt (p3,q1))) + (sqr q1)),(sqr p3)) is set
(sqr p3) + (2 * (mlt (p3,q1))) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),(sqr p3),(2 * (mlt (p3,q1)))) is set
((sqr p3) + (2 * (mlt (p3,q1)))) + (sqr q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),((sqr p3) + (2 * (mlt (p3,q1)))),(sqr q1)) is set
p3 - q1 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),p3,q1) is set
K325(q1) is V16() Function-like complex-valued set
K163() * q1 is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * q1 is V16() Function-like set
K369(K38(1)) * q1 is V16() Function-like complex-valued ext-real-valued real-valued set
K296(p3,K325(q1)) is V16() Function-like set
sqr (p3 - q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
sqrreal * (p3 - q1) is V16() Function-like complex-valued ext-real-valued real-valued set
mlt ((p3 - q1),(p3 - q1)) is V16() Function-like set
K203(K167(),(p3 - q1),(p3 - q1)) is set
(((sqr p3) + (2 * (mlt (p3,q1)))) + (sqr q1)) - (sqr (p3 - q1)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(((sqr p3) + (2 * (mlt (p3,q1)))) + (sqr q1)),(sqr (p3 - q1))) is set
K325((sqr (p3 - q1))) is V16() Function-like complex-valued set
K163() * (sqr (p3 - q1)) is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * (sqr (p3 - q1)) is V16() Function-like set
K369(K38(1)) * (sqr (p3 - q1)) is V16() Function-like complex-valued ext-real-valued real-valued set
K296((((sqr p3) + (2 * (mlt (p3,q1)))) + (sqr q1)),K325((sqr (p3 - q1)))) is V16() Function-like set
(sqr p3) - (2 * (mlt (p3,q1))) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(sqr p3),(2 * (mlt (p3,q1)))) is set
K325((2 * (mlt (p3,q1)))) is V16() Function-like complex-valued set
K163() * (2 * (mlt (p3,q1))) is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * (2 * (mlt (p3,q1))) is V16() Function-like set
K369(K38(1)) * (2 * (mlt (p3,q1))) is V16() Function-like complex-valued ext-real-valued real-valued set
K296((sqr p3),K325((2 * (mlt (p3,q1))))) is V16() Function-like set
((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),((sqr p3) - (2 * (mlt (p3,q1)))),(sqr q1)) is set
(((sqr p3) + (2 * (mlt (p3,q1)))) + (sqr q1)) - (((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(((sqr p3) + (2 * (mlt (p3,q1)))) + (sqr q1)),(((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1))) is set
K325((((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1))) is V16() Function-like complex-valued set
K163() * (((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1)) is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * (((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1)) is V16() Function-like set
K369(K38(1)) * (((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1)) is V16() Function-like complex-valued ext-real-valued real-valued set
K296((((sqr p3) + (2 * (mlt (p3,q1)))) + (sqr q1)),K325((((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1)))) is V16() Function-like set
(((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - (((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)),(((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1))) is set
K296((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)),K325((((sqr p3) - (2 * (mlt (p3,q1)))) + (sqr q1)))) is V16() Function-like set
(((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - ((sqr p3) - (2 * (mlt (p3,q1)))) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)),((sqr p3) - (2 * (mlt (p3,q1))))) is set
K325(((sqr p3) - (2 * (mlt (p3,q1))))) is V16() Function-like complex-valued set
K163() * ((sqr p3) - (2 * (mlt (p3,q1)))) is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * ((sqr p3) - (2 * (mlt (p3,q1)))) is V16() Function-like set
K369(K38(1)) * ((sqr p3) - (2 * (mlt (p3,q1)))) is V16() Function-like complex-valued ext-real-valued real-valued set
K296((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)),K325(((sqr p3) - (2 * (mlt (p3,q1)))))) is V16() Function-like set
((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - ((sqr p3) - (2 * (mlt (p3,q1))))) - (sqr q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - ((sqr p3) - (2 * (mlt (p3,q1))))),(sqr q1)) is set
K325((sqr q1)) is V16() Function-like complex-valued set
K163() * (sqr q1) is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * (sqr q1) is V16() Function-like set
K369(K38(1)) * (sqr q1) is V16() Function-like complex-valued ext-real-valued real-valued set
K296(((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - ((sqr p3) - (2 * (mlt (p3,q1))))),K325((sqr q1))) is V16() Function-like set
(((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - (sqr p3) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)),(sqr p3)) is set
K325((sqr p3)) is V16() Function-like complex-valued set
K163() * (sqr p3) is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * (sqr p3) is V16() Function-like set
K369(K38(1)) * (sqr p3) is V16() Function-like complex-valued ext-real-valued real-valued set
K296((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)),K325((sqr p3))) is V16() Function-like set
((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - (sqr p3)) + (2 * (mlt (p3,q1))) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K165(),((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - (sqr p3)),(2 * (mlt (p3,q1)))) is set
(((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - (sqr p3)) + (2 * (mlt (p3,q1)))) - (sqr q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - (sqr p3)) + (2 * (mlt (p3,q1)))),(sqr q1)) is set
K296((((((2 * (mlt (p3,q1))) + (sqr q1)) + (sqr p3)) - (sqr p3)) + (2 * (mlt (p3,q1)))),K325((sqr q1))) is V16() Function-like set
(((2 * (mlt (p3,q1))) + (sqr q1)) + (2 * (mlt (p3,q1)))) - (sqr q1) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K203(K166(),(((2 * (mlt (p3,q1))) + (sqr q1)) + (2 * (mlt (p3,q1)))),(sqr q1)) is set
K296((((2 * (mlt (p3,q1))) + (sqr q1)) + (2 * (mlt (p3,q1)))),K325((sqr q1))) is V16() Function-like set
2 + 2 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
(2 + 2) * (mlt (p3,q1)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K369((2 + 2)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),(2 + 2),K83(REAL)) is set
K369((2 + 2)) * (mlt (p3,q1)) is V16() Function-like complex-valued ext-real-valued real-valued set
4 * (mlt (p3,q1)) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K369(4) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),4,K83(REAL)) is set
K369(4) * (mlt (p3,q1)) is V16() Function-like complex-valued ext-real-valued real-valued set
Sum (mlt (p3,q1)) is V11() real ext-real M2( REAL )
4 * (Sum (mlt (p3,q1))) is V11() real ext-real M2( REAL )
(1 / 4) * (4 * (Sum (mlt (p3,q1)))) is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
rng n is V129() V130() V131() M2(K6(REAL))
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
|.n.| is V11() real ext-real non negative M2( REAL )
|.n.| ^2 is V11() real ext-real M2( REAL )
K37(|.n.|,|.n.|) is V11() real ext-real non negative set
|(n,n)| is V11() real ext-real M2( REAL )
mlt (n,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),n,n) is set
Sum (mlt (n,n)) is V11() real ext-real M2( REAL )
sqr n is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
sqrreal is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
sqrreal * n is V16() Function-like complex-valued ext-real-valued real-valued set
mlt (n,n) is V16() Function-like set
Sum (sqr n) is V11() real ext-real M2( REAL )
sqrt (Sum (sqr n)) is V11() real ext-real M2( REAL )
(sqrt (Sum (sqr n))) ^2 is V11() real ext-real M2( REAL )
K37((sqrt (Sum (sqr n))),(sqrt (Sum (sqr n)))) is V11() real ext-real set
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
|.n.| is V11() real ext-real non negative M2( REAL )
|(n,n)| is V11() real ext-real M2( REAL )
mlt (n,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),n,n) is set
Sum (mlt (n,n)) is V11() real ext-real M2( REAL )
sqrt |(n,n)| is V11() real ext-real M2( REAL )
|.n.| ^2 is V11() real ext-real M2( REAL )
K37(|.n.|,|.n.|) is V11() real ext-real non negative set
sqrt (|.n.| ^2) is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
|.n.| is V11() real ext-real non negative M2( REAL )
|(n,n)| is V11() real ext-real M2( REAL )
mlt (n,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),n,n) is set
Sum (mlt (n,n)) is V11() real ext-real M2( REAL )
sqrt |(n,n)| is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
|(n,n)| is V11() real ext-real M2( REAL )
mlt (n,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),n,n) is set
Sum (mlt (n,n)) is V11() real ext-real M2( REAL )
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
0* (len n) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44( len n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (len n)
REAL (len n) is V1() functional FinSequence-membered FinSequenceSet of REAL
|.n.| is V11() real ext-real non negative M2( REAL )
|.n.| ^2 is V11() real ext-real M2( REAL )
K37(|.n.|,|.n.|) is V11() real ext-real non negative set
p is V16() V19( NAT ) V20( REAL ) Function-like V37() V44( len n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (len n)
|.n.| is V11() real ext-real non negative M2( REAL )
0 ^2 is V11() real ext-real M2( REAL )
K37(0,0) is V11() real ext-real set
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
|(n,n)| is V11() real ext-real M2( REAL )
mlt (n,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),n,n) is set
Sum (mlt (n,n)) is V11() real ext-real M2( REAL )
|.n.| is V11() real ext-real non negative M2( REAL )
0 ^2 is V11() real ext-real M2( REAL )
K37(0,0) is V11() real ext-real set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
0* (len n) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44( len n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (len n)
REAL (len n) is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
0* (len n) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44( len n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (len n)
REAL (len n) is V1() functional FinSequence-membered FinSequenceSet of REAL
|(n,(0* (len n)))| is V11() real ext-real M2( REAL )
mlt (n,(0* (len n))) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),n,(0* (len n))) is set
Sum (mlt (n,(0* (len n)))) is V11() real ext-real M2( REAL )
(len n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
REAL * is V1() functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = len n } is set
(len n) |-> 0 is V16() empty-yielding V19( NAT ) V20( REAL ) Function-like V37() V44( len n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n) -tuples_on REAL
Seg (len n) is V37() V44( len n) V129() V130() V131() V132() V133() V134() M2(K6(NAT))
K207((Seg (len n)),0) is V16() V19( Seg (len n)) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg (len n),{0}) V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued M2(K6(K7((Seg (len n)),{0})))
{0} is V129() V130() V131() V132() V133() V134() set
K7((Seg (len n)),{0}) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (len n)),{0})) is set
p is V16() V19( NAT ) V20( REAL ) Function-like V37() V44( len n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n) -tuples_on REAL
mlt (p,(0* (len n))) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,(0* (len n))) is set
Sum (mlt (p,(0* (len n)))) is V11() real ext-real M2( REAL )
Sum (0* (len n)) is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
0* (len n) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44( len n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (len n)
REAL (len n) is V1() functional FinSequence-membered FinSequenceSet of REAL
|((0* (len n)),n)| is V11() real ext-real M2( REAL )
mlt ((0* (len n)),n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),(0* (len n)),n) is set
Sum (mlt ((0* (len n)),n)) is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
p is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),n,p) is set
|.(n + p).| is V11() real ext-real non negative M2( REAL )
|.(n + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(n + p).|,|.(n + p).|) is V11() real ext-real non negative set
|.n.| is V11() real ext-real non negative M2( REAL )
|.n.| ^2 is V11() real ext-real M2( REAL )
K37(|.n.|,|.n.|) is V11() real ext-real non negative set
|(p,n)| is V11() real ext-real M2( REAL )
mlt (p,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,n) is set
Sum (mlt (p,n)) is V11() real ext-real M2( REAL )
2 * |(p,n)| is V11() real ext-real M2( REAL )
(|.n.| ^2) + (2 * |(p,n)|) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
((|.n.| ^2) + (2 * |(p,n)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
|((n + p),(n + p))| is V11() real ext-real M2( REAL )
mlt ((n + p),(n + p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(n + p),(n + p)) is set
Sum (mlt ((n + p),(n + p))) is V11() real ext-real M2( REAL )
|(n,n)| is V11() real ext-real M2( REAL )
mlt (n,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),n,n) is set
Sum (mlt (n,n)) is V11() real ext-real M2( REAL )
|(n,p)| is V11() real ext-real M2( REAL )
mlt (n,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),n,p) is set
Sum (mlt (n,p)) is V11() real ext-real M2( REAL )
2 * |(n,p)| is V11() real ext-real M2( REAL )
|(n,n)| + (2 * |(n,p)|) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
(|(n,n)| + (2 * |(n,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
((|.n.| ^2) + (2 * |(p,n)|)) + |(p,p)| is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
p is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),n,p) is set
K325(p) is V16() Function-like complex-valued set
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K296(n,K325(p)) is V16() Function-like set
|.(n - p).| is V11() real ext-real non negative M2( REAL )
|.(n - p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(n - p).|,|.(n - p).|) is V11() real ext-real non negative set
|.n.| is V11() real ext-real non negative M2( REAL )
|.n.| ^2 is V11() real ext-real M2( REAL )
K37(|.n.|,|.n.|) is V11() real ext-real non negative set
|(p,n)| is V11() real ext-real M2( REAL )
mlt (p,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,n) is set
Sum (mlt (p,n)) is V11() real ext-real M2( REAL )
2 * |(p,n)| is V11() real ext-real M2( REAL )
(|.n.| ^2) - (2 * |(p,n)|) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
((|.n.| ^2) - (2 * |(p,n)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
|((n - p),(n - p))| is V11() real ext-real M2( REAL )
mlt ((n - p),(n - p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(n - p),(n - p)) is set
Sum (mlt ((n - p),(n - p))) is V11() real ext-real M2( REAL )
|(n,n)| is V11() real ext-real M2( REAL )
mlt (n,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),n,n) is set
Sum (mlt (n,n)) is V11() real ext-real M2( REAL )
|(n,p)| is V11() real ext-real M2( REAL )
mlt (n,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),n,p) is set
Sum (mlt (n,p)) is V11() real ext-real M2( REAL )
2 * |(n,p)| is V11() real ext-real M2( REAL )
|(n,n)| - (2 * |(n,p)|) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
(|(n,n)| - (2 * |(n,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
((|.n.| ^2) - (2 * |(p,n)|)) + |(p,p)| is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
p is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),n,p) is set
|.(n + p).| is V11() real ext-real non negative M2( REAL )
|.(n + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(n + p).|,|.(n + p).|) is V11() real ext-real non negative set
n - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),n,p) is set
K325(p) is V16() Function-like complex-valued set
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K296(n,K325(p)) is V16() Function-like set
|.(n - p).| is V11() real ext-real non negative M2( REAL )
|.(n - p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(n - p).|,|.(n - p).|) is V11() real ext-real non negative set
(|.(n + p).| ^2) + (|.(n - p).| ^2) is V11() real ext-real M2( REAL )
|.n.| is V11() real ext-real non negative M2( REAL )
|.n.| ^2 is V11() real ext-real M2( REAL )
K37(|.n.|,|.n.|) is V11() real ext-real non negative set
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
(|.n.| ^2) + (|.p.| ^2) is V11() real ext-real M2( REAL )
2 * ((|.n.| ^2) + (|.p.| ^2)) is V11() real ext-real M2( REAL )
|(p,n)| is V11() real ext-real M2( REAL )
mlt (p,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,n) is set
Sum (mlt (p,n)) is V11() real ext-real M2( REAL )
2 * |(p,n)| is V11() real ext-real M2( REAL )
(|.n.| ^2) + (2 * |(p,n)|) is V11() real ext-real M2( REAL )
((|.n.| ^2) + (2 * |(p,n)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.n.| ^2) + (2 * |(p,n)|)) + (|.p.| ^2)) + (|.(n - p).| ^2) is V11() real ext-real M2( REAL )
|(n,p)| is V11() real ext-real M2( REAL )
mlt (n,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),n,p) is set
Sum (mlt (n,p)) is V11() real ext-real M2( REAL )
2 * |(n,p)| is V11() real ext-real M2( REAL )
(|.n.| ^2) + (2 * |(n,p)|) is V11() real ext-real M2( REAL )
((|.n.| ^2) + (2 * |(n,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(|.n.| ^2) - (2 * |(p,n)|) is V11() real ext-real M2( REAL )
((|.n.| ^2) - (2 * |(p,n)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.n.| ^2) + (2 * |(n,p)|)) + (|.p.| ^2)) + (((|.n.| ^2) - (2 * |(p,n)|)) + (|.p.| ^2)) is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
p is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),n,p) is set
|.(n + p).| is V11() real ext-real non negative M2( REAL )
|.(n + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(n + p).|,|.(n + p).|) is V11() real ext-real non negative set
n - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),n,p) is set
K325(p) is V16() Function-like complex-valued set
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K296(n,K325(p)) is V16() Function-like set
|.(n - p).| is V11() real ext-real non negative M2( REAL )
|.(n - p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(n - p).|,|.(n - p).|) is V11() real ext-real non negative set
(|.(n + p).| ^2) - (|.(n - p).| ^2) is V11() real ext-real M2( REAL )
|(n,p)| is V11() real ext-real M2( REAL )
mlt (n,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),n,p) is set
Sum (mlt (n,p)) is V11() real ext-real M2( REAL )
4 * |(n,p)| is V11() real ext-real M2( REAL )
|.n.| is V11() real ext-real non negative M2( REAL )
|.n.| ^2 is V11() real ext-real M2( REAL )
K37(|.n.|,|.n.|) is V11() real ext-real non negative set
|(p,n)| is V11() real ext-real M2( REAL )
mlt (p,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,n) is set
Sum (mlt (p,n)) is V11() real ext-real M2( REAL )
2 * |(p,n)| is V11() real ext-real M2( REAL )
(|.n.| ^2) + (2 * |(p,n)|) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
((|.n.| ^2) + (2 * |(p,n)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.n.| ^2) + (2 * |(p,n)|)) + (|.p.| ^2)) - (|.(n - p).| ^2) is V11() real ext-real M2( REAL )
2 * |(n,p)| is V11() real ext-real M2( REAL )
(|.n.| ^2) + (2 * |(n,p)|) is V11() real ext-real M2( REAL )
((|.n.| ^2) + (2 * |(n,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(|.n.| ^2) - (2 * |(p,n)|) is V11() real ext-real M2( REAL )
((|.n.| ^2) - (2 * |(p,n)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.n.| ^2) + (2 * |(n,p)|)) + (|.p.| ^2)) - (((|.n.| ^2) - (2 * |(p,n)|)) + (|.p.| ^2)) is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
p is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
|(n,p)| is V11() real ext-real M2( REAL )
mlt (n,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),n,p) is set
Sum (mlt (n,p)) is V11() real ext-real M2( REAL )
abs |(n,p)| is V11() real ext-real M2( REAL )
|.n.| is V11() real ext-real non negative M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.n.| * |.p.| is V11() real ext-real non negative M2( REAL )
0* (len n) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44( len n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (len n)
REAL (len n) is V1() functional FinSequence-membered FinSequenceSet of REAL
|(n,n)| is V11() real ext-real M2( REAL )
mlt (n,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),n,n) is set
Sum (mlt (n,n)) is V11() real ext-real M2( REAL )
sqrt |(n,n)| is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
sqrt |(p,p)| is V11() real ext-real M2( REAL )
(sqrt |(n,n)|) * (sqrt |(p,p)|) is V11() real ext-real M2( REAL )
2 * |(n,p)| is V11() real ext-real M2( REAL )
p is V11() real ext-real set
p ^2 is V11() real ext-real set
K37(p,p) is V11() real ext-real set
|(n,n)| * (p ^2) is V11() real ext-real M2( REAL )
(2 * |(n,p)|) * p is V11() real ext-real M2( REAL )
(|(n,n)| * (p ^2)) + ((2 * |(n,p)|) * p) is V11() real ext-real M2( REAL )
((|(n,n)| * (p ^2)) + ((2 * |(n,p)|) * p)) + |(p,p)| is V11() real ext-real M2( REAL )
p * n is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K369(p) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),p,K83(REAL)) is set
K369(p) * n is V16() Function-like complex-valued ext-real-valued real-valued set
len (p * n) is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
(p * n) + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),(p * n),p) is set
|(((p * n) + p),((p * n) + p))| is V11() real ext-real M2( REAL )
mlt (((p * n) + p),((p * n) + p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),((p * n) + p),((p * n) + p)) is set
Sum (mlt (((p * n) + p),((p * n) + p))) is V11() real ext-real M2( REAL )
|((p * n),(p * n))| is V11() real ext-real M2( REAL )
mlt ((p * n),(p * n)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p * n),(p * n)) is set
Sum (mlt ((p * n),(p * n))) is V11() real ext-real M2( REAL )
|((p * n),p)| is V11() real ext-real M2( REAL )
mlt ((p * n),p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p * n),p) is set
Sum (mlt ((p * n),p)) is V11() real ext-real M2( REAL )
2 * |((p * n),p)| is V11() real ext-real M2( REAL )
|((p * n),(p * n))| + (2 * |((p * n),p)|) is V11() real ext-real M2( REAL )
(|((p * n),(p * n))| + (2 * |((p * n),p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
|((p * n),n)| is V11() real ext-real M2( REAL )
mlt ((p * n),n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p * n),n) is set
Sum (mlt ((p * n),n)) is V11() real ext-real M2( REAL )
p * |((p * n),n)| is V11() real ext-real M2( REAL )
(p * |((p * n),n)|) + (2 * |((p * n),p)|) is V11() real ext-real M2( REAL )
((p * |((p * n),n)|) + (2 * |((p * n),p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
p * |(n,n)| is V11() real ext-real M2( REAL )
p * (p * |(n,n)|) is V11() real ext-real M2( REAL )
(p * (p * |(n,n)|)) + (2 * |((p * n),p)|) is V11() real ext-real M2( REAL )
((p * (p * |(n,n)|)) + (2 * |((p * n),p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
|(n,p)| * p is V11() real ext-real M2( REAL )
2 * (|(n,p)| * p) is V11() real ext-real M2( REAL )
(|(n,n)| * (p ^2)) + (2 * (|(n,p)| * p)) is V11() real ext-real M2( REAL )
((|(n,n)| * (p ^2)) + (2 * (|(n,p)| * p))) + |(p,p)| is V11() real ext-real M2( REAL )
delta (|(n,n)|,(2 * |(n,p)|),|(p,p)|) is V11() real ext-real M2( REAL )
(2 * |(n,p)|) ^2 is V11() real ext-real M2( REAL )
K37((2 * |(n,p)|),(2 * |(n,p)|)) is V11() real ext-real set
4 * |(n,n)| is V11() real ext-real M2( REAL )
(4 * |(n,n)|) * |(p,p)| is V11() real ext-real M2( REAL )
((2 * |(n,p)|) ^2) - ((4 * |(n,n)|) * |(p,p)|) is V11() real ext-real M2( REAL )
|(n,p)| ^2 is V11() real ext-real M2( REAL )
K37(|(n,p)|,|(n,p)|) is V11() real ext-real set
|(n,n)| * |(p,p)| is V11() real ext-real M2( REAL )
(|(n,p)| ^2) - (|(n,n)| * |(p,p)|) is V11() real ext-real M2( REAL )
4 * ((|(n,p)| ^2) - (|(n,n)| * |(p,p)|)) is V11() real ext-real M2( REAL )
0 / 4 is V11() real ext-real V34() M2( RAT )
(abs |(n,p)|) ^2 is V11() real ext-real M2( REAL )
K37((abs |(n,p)|),(abs |(n,p)|)) is V11() real ext-real set
sqrt ((abs |(n,p)|) ^2) is V11() real ext-real M2( REAL )
sqrt (|(n,n)| * |(p,p)|) is V11() real ext-real M2( REAL )
n is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len n is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
p is V16() V19( NAT ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),n,p) is set
|.(n + p).| is V11() real ext-real non negative M2( REAL )
|.n.| is V11() real ext-real non negative M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.n.| + |.p.| is V11() real ext-real non negative M2( REAL )
|(n,p)| is V11() real ext-real M2( REAL )
mlt (n,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),n,p) is set
Sum (mlt (n,p)) is V11() real ext-real M2( REAL )
abs |(n,p)| is V11() real ext-real M2( REAL )
|.n.| * |.p.| is V11() real ext-real non negative M2( REAL )
2 * |(n,p)| is V11() real ext-real M2( REAL )
2 * (|.n.| * |.p.|) is V11() real ext-real M2( REAL )
|.n.| ^2 is V11() real ext-real M2( REAL )
K37(|.n.|,|.n.|) is V11() real ext-real non negative set
(|.n.| ^2) + (2 * |(n,p)|) is V11() real ext-real M2( REAL )
(|.n.| ^2) + (2 * (|.n.| * |.p.|)) is V11() real ext-real M2( REAL )
|.(n + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(n + p).|,|.(n + p).|) is V11() real ext-real non negative set
|(p,n)| is V11() real ext-real M2( REAL )
mlt (p,n) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,n) is set
Sum (mlt (p,n)) is V11() real ext-real M2( REAL )
2 * |(p,n)| is V11() real ext-real M2( REAL )
(|.n.| ^2) + (2 * |(p,n)|) is V11() real ext-real M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
((|.n.| ^2) + (2 * |(p,n)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
2 * |.n.| is V11() real ext-real M2( REAL )
(2 * |.n.|) * |.p.| is V11() real ext-real M2( REAL )
(|.n.| ^2) + ((2 * |.n.|) * |.p.|) is V11() real ext-real M2( REAL )
((|.n.| ^2) + ((2 * |.n.|) * |.p.|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
sqrt (|.(n + p).| ^2) is V11() real ext-real M2( REAL )
(|.n.| + |.p.|) ^2 is V11() real ext-real M2( REAL )
K37((|.n.| + |.p.|),(|.n.| + |.p.|)) is V11() real ext-real non negative set
sqrt ((|.n.| + |.p.|) ^2) is V11() real ext-real M2( REAL )
0 + 0 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
|.(p + p).| is V11() real ext-real non negative M2( REAL )
|.(p + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p + p).|,|.(p + p).|) is V11() real ext-real non negative set
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
|.(p - p).| is V11() real ext-real non negative M2( REAL )
|.(p - p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p - p).|,|.(p - p).|) is V11() real ext-real non negative set
(|.(p + p).| ^2) - (|.(p - p).| ^2) is V11() real ext-real M2( REAL )
(1 / 4) * ((|.(p + p).| ^2) - (|.(p - p).| ^2)) is V11() real ext-real M2( REAL )
REAL n is V1() functional FinSequence-membered FinSequenceSet of REAL
q is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
q + q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
K203(K165(),q,q2) is set
|.(q + q2).| is V11() real ext-real non negative M2( REAL )
|.(q + q2).| ^2 is V11() real ext-real M2( REAL )
K37(|.(q + q2).|,|.(q + q2).|) is V11() real ext-real non negative set
q - q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n
K203(K166(),q,q2) is set
K325(q2) is V16() Function-like complex-valued set
K163() * q2 is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * q2 is V16() Function-like set
K369(K38(1)) * q2 is V16() Function-like complex-valued ext-real-valued real-valued set
K296(q,K325(q2)) is V16() Function-like set
|.(q - q2).| is V11() real ext-real non negative M2( REAL )
|.(q - q2).| ^2 is V11() real ext-real M2( REAL )
K37(|.(q - q2).|,|.(q - q2).|) is V11() real ext-real non negative set
(|.(q + q2).| ^2) - (|.(q - q2).| ^2) is V11() real ext-real M2( REAL )
(1 / 4) * ((|.(q + q2).| ^2) - (|.(q - q2).| ^2)) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|((p + p),q)| is V11() real ext-real M2( REAL )
mlt ((p + p),q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),(p + p),q) is set
Sum (mlt ((p + p),q)) is V11() real ext-real M2( REAL )
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
|(p,q)| + |(p,q)| is V11() real ext-real M2( REAL )
REAL n is V1() functional FinSequence-membered FinSequenceSet of REAL
p3 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len p3 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len q2 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
q1 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len q1 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
q is V11() real ext-real set
q * p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q * p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K369(q) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),q,K83(REAL)) is set
K369(q) * p is V16() Function-like complex-valued ext-real-valued real-valued set
|((q * p),p)| is V11() real ext-real M2( REAL )
mlt ((q * p),p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(q * p),p) is set
Sum (mlt ((q * p),p)) is V11() real ext-real M2( REAL )
q * |(p,p)| is V11() real ext-real M2( REAL )
REAL n is V1() functional FinSequence-membered FinSequenceSet of REAL
q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len q2 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
p3 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len p3 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q is V11() real ext-real set
q * p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q * p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K369(q) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),q,K83(REAL)) is set
K369(q) * p is V16() Function-like complex-valued ext-real-valued real-valued set
|(p,(q * p))| is V11() real ext-real M2( REAL )
mlt (p,(q * p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,(q * p)) is set
Sum (mlt (p,(q * p))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
q * |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|((- p),p)| is V11() real ext-real M2( REAL )
mlt ((- p),p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(- p),p) is set
Sum (mlt ((- p),p)) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
- |(p,p)| is V11() real ext-real M2( REAL )
- 1 is V11() real ext-real V33() V34() M2( INT )
(- 1) * p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
(- 1) * p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K369((- 1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),(- 1),K83(REAL)) is set
K369((- 1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
|(((- 1) * p),p)| is V11() real ext-real M2( REAL )
mlt (((- 1) * p),p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),((- 1) * p),p) is set
Sum (mlt (((- 1) * p),p)) is V11() real ext-real M2( REAL )
(- 1) * |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
|(p,(- p))| is V11() real ext-real M2( REAL )
mlt (p,(- p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,(- p)) is set
Sum (mlt (p,(- p))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
- |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * p is V16() Function-like set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
|((- p),(- p))| is V11() real ext-real M2( REAL )
mlt ((- p),(- p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(- p),(- p)) is set
Sum (mlt ((- p),(- p))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|(p,(- p))| is V11() real ext-real M2( REAL )
mlt (p,(- p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,(- p)) is set
Sum (mlt (p,(- p))) is V11() real ext-real M2( REAL )
- |(p,(- p))| is V11() real ext-real M2( REAL )
- |(p,p)| is V11() real ext-real M2( REAL )
- (- |(p,p)|) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|((p - p),q)| is V11() real ext-real M2( REAL )
mlt ((p - p),q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p - p),q) is set
Sum (mlt ((p - p),q)) is V11() real ext-real M2( REAL )
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
|(p,q)| - |(p,q)| is V11() real ext-real M2( REAL )
|((- p),q)| is V11() real ext-real M2( REAL )
mlt ((- p),q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(- p),q) is set
Sum (mlt ((- p),q)) is V11() real ext-real M2( REAL )
|(p,q)| + |((- p),q)| is V11() real ext-real M2( REAL )
- |(p,q)| is V11() real ext-real M2( REAL )
|(p,q)| + (- |(p,q)|) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V11() real ext-real set
p is V11() real ext-real set
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p * q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p * q is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K369(p) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),p,K83(REAL)) is set
K369(p) * q is V16() Function-like complex-valued ext-real-valued real-valued set
q2 is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p * q2 is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p * q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K369(p) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),p,K83(REAL)) is set
K369(p) * q2 is V16() Function-like complex-valued ext-real-valued real-valued set
(p * q) + (p * q2) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),(p * q),(p * q2)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
(p * q) + (p * q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),(p * q),(p * q2)) is set
p3 is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(((p * q) + (p * q2)),p3)| is V11() real ext-real M2( REAL )
mlt (((p * q) + (p * q2)),p3) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),((p * q) + (p * q2)),p3) is set
Sum (mlt (((p * q) + (p * q2)),p3)) is V11() real ext-real M2( REAL )
|(q,p3)| is V11() real ext-real M2( REAL )
mlt (q,p3) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),q,p3) is set
Sum (mlt (q,p3)) is V11() real ext-real M2( REAL )
p * |(q,p3)| is V11() real ext-real M2( REAL )
|(q2,p3)| is V11() real ext-real M2( REAL )
mlt (q2,p3) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),q2,p3) is set
Sum (mlt (q2,p3)) is V11() real ext-real M2( REAL )
p * |(q2,p3)| is V11() real ext-real M2( REAL )
(p * |(q,p3)|) + (p * |(q2,p3)|) is V11() real ext-real M2( REAL )
|((p * q),p3)| is V11() real ext-real M2( REAL )
mlt ((p * q),p3) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p * q),p3) is set
Sum (mlt ((p * q),p3)) is V11() real ext-real M2( REAL )
|((p * q2),p3)| is V11() real ext-real M2( REAL )
mlt ((p * q2),p3) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p * q2),p3) is set
Sum (mlt ((p * q2),p3)) is V11() real ext-real M2( REAL )
|((p * q),p3)| + |((p * q2),p3)| is V11() real ext-real M2( REAL )
(p * |(q,p3)|) + |((p * q2),p3)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,q) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + q is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,q) is set
|(p,(p + q))| is V11() real ext-real M2( REAL )
mlt (p,(p + q)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,(p + q)) is set
Sum (mlt (p,(p + q))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
|(p,p)| + |(p,q)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p - q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- q is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * q is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * q is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * q is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- q)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- q)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,(- q)) is set
p - q is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,q) is set
K325(q) is V16() Function-like complex-valued set
K296(p,K325(q)) is V16() Function-like set
|(p,(p - q))| is V11() real ext-real M2( REAL )
mlt (p,(p - q)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,(p - q)) is set
Sum (mlt (p,(p - q))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
|(p,p)| - |(p,q)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
q2 is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q + q2 is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),q,q2) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q + q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K165(),q,q2) is set
|((p + p),(q + q2))| is V11() real ext-real M2( REAL )
mlt ((p + p),(q + q2)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p + p),(q + q2)) is set
Sum (mlt ((p + p),(q + q2))) is V11() real ext-real M2( REAL )
|(p,q2)| is V11() real ext-real M2( REAL )
mlt (p,q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q2) is set
Sum (mlt (p,q2)) is V11() real ext-real M2( REAL )
|(p,q)| + |(p,q2)| is V11() real ext-real M2( REAL )
(|(p,q)| + |(p,q2)|) + |(p,q)| is V11() real ext-real M2( REAL )
|(p,q2)| is V11() real ext-real M2( REAL )
mlt (p,q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q2) is set
Sum (mlt (p,q2)) is V11() real ext-real M2( REAL )
((|(p,q)| + |(p,q2)|) + |(p,q)|) + |(p,q2)| is V11() real ext-real M2( REAL )
|((p + p),q)| is V11() real ext-real M2( REAL )
mlt ((p + p),q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p + p),q) is set
Sum (mlt ((p + p),q)) is V11() real ext-real M2( REAL )
|(p,q)| + |(p,q)| is V11() real ext-real M2( REAL )
|((p + p),q2)| is V11() real ext-real M2( REAL )
mlt ((p + p),q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p + p),q2) is set
Sum (mlt ((p + p),q2)) is V11() real ext-real M2( REAL )
|(p,q2)| + |(p,q2)| is V11() real ext-real M2( REAL )
|((p + p),q)| + |((p + p),q2)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
q2 is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q - q2 is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- q2 is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() * q2 is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) * q2 is V16() Function-like set
K369(K38(1)) * q2 is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),q,(- q2)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),q,(- q2)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q + (- q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K165(),q,(- q2)) is set
q - q2 is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K166(),q,q2) is set
K325(q2) is V16() Function-like complex-valued set
K296(q,K325(q2)) is V16() Function-like set
|((p - p),(q - q2))| is V11() real ext-real M2( REAL )
mlt ((p - p),(q - q2)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p - p),(q - q2)) is set
Sum (mlt ((p - p),(q - q2))) is V11() real ext-real M2( REAL )
|(p,q2)| is V11() real ext-real M2( REAL )
mlt (p,q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q2) is set
Sum (mlt (p,q2)) is V11() real ext-real M2( REAL )
|(p,q)| - |(p,q2)| is V11() real ext-real M2( REAL )
(|(p,q)| - |(p,q2)|) - |(p,q)| is V11() real ext-real M2( REAL )
|(p,q2)| is V11() real ext-real M2( REAL )
mlt (p,q2) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q2) is set
Sum (mlt (p,q2)) is V11() real ext-real M2( REAL )
((|(p,q)| - |(p,q2)|) - |(p,q)|) + |(p,q2)| is V11() real ext-real M2( REAL )
|(p,(q - q2))| is V11() real ext-real M2( REAL )
mlt (p,(q - q2)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,(q - q2)) is set
Sum (mlt (p,(q - q2))) is V11() real ext-real M2( REAL )
|(p,(q - q2))| is V11() real ext-real M2( REAL )
mlt (p,(q - q2)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,(q - q2)) is set
Sum (mlt (p,(q - q2))) is V11() real ext-real M2( REAL )
|(p,q)| - |(p,q2)| is V11() real ext-real M2( REAL )
|(p,(q - q2))| - |(p,(q - q2))| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
|((p + p),(p + p))| is V11() real ext-real M2( REAL )
mlt ((p + p),(p + p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p + p),(p + p)) is set
Sum (mlt ((p + p),(p + p))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
2 * |(p,p)| is V11() real ext-real M2( REAL )
|(p,p)| + (2 * |(p,p)|) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
(|(p,p)| + (2 * |(p,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
|(p,p)| + |(p,p)| is V11() real ext-real M2( REAL )
(|(p,p)| + |(p,p)|) + |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
|((p - p),(p - p))| is V11() real ext-real M2( REAL )
mlt ((p - p),(p - p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p - p),(p - p)) is set
Sum (mlt ((p - p),(p - p))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
2 * |(p,p)| is V11() real ext-real M2( REAL )
|(p,p)| - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
(|(p,p)| - (2 * |(p,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
|(p,p)| - |(p,p)| is V11() real ext-real M2( REAL )
(|(p,p)| - |(p,p)|) - |(p,p)| is V11() real ext-real M2( REAL )
((|(p,p)| - |(p,p)|) - |(p,p)|) + |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,(0. (TOP-REAL n)))| is V11() real ext-real M2( REAL )
mlt (p,(0. (TOP-REAL n))) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,(0. (TOP-REAL n))) is set
Sum (mlt (p,(0. (TOP-REAL n)))) is V11() real ext-real M2( REAL )
p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
0* (len p) is V16() V19( NAT ) V20( REAL ) Function-like V37() V44( len p) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (len p)
REAL (len p) is V1() functional FinSequence-membered FinSequenceSet of REAL
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|((0. (TOP-REAL n)),p)| is V11() real ext-real M2( REAL )
mlt ((0. (TOP-REAL n)),p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),(0. (TOP-REAL n)),p) is set
Sum (mlt ((0. (TOP-REAL n)),p)) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U1 of (TOP-REAL n) is set
|((0. (TOP-REAL n)),(0. (TOP-REAL n)))| is V11() real ext-real M2( REAL )
mlt ((0. (TOP-REAL n)),(0. (TOP-REAL n))) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),(0. (TOP-REAL n)),(0. (TOP-REAL n))) is set
Sum (mlt ((0. (TOP-REAL n)),(0. (TOP-REAL n)))) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
sqrt |(p,p)| is V11() real ext-real M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
sqrt (|.p.| ^2) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
sqrt |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U1 of (TOP-REAL n) is set
|.(0. (TOP-REAL n)).| is V11() real ext-real non negative M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
0 ^2 is V11() real ext-real M2( REAL )
K37(0,0) is V11() real ext-real set
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
|.(p + p).| is V11() real ext-real non negative M2( REAL )
|.(p + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p + p).|,|.(p + p).|) is V11() real ext-real non negative set
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
2 * |(p,p)| is V11() real ext-real M2( REAL )
(|.p.| ^2) + (2 * |(p,p)|) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
|((p + p),(p + p))| is V11() real ext-real M2( REAL )
mlt ((p + p),(p + p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p + p),(p + p)) is set
Sum (mlt ((p + p),(p + p))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|(p,p)| + (2 * |(p,p)|) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
(|(p,p)| + (2 * |(p,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
((|.p.| ^2) + (2 * |(p,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
|.(p - p).| is V11() real ext-real non negative M2( REAL )
|.(p - p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p - p).|,|.(p - p).|) is V11() real ext-real non negative set
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
2 * |(p,p)| is V11() real ext-real M2( REAL )
(|.p.| ^2) - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
((|.p.| ^2) - (2 * |(p,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
|((p - p),(p - p))| is V11() real ext-real M2( REAL )
mlt ((p - p),(p - p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p - p),(p - p)) is set
Sum (mlt ((p - p),(p - p))) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|(p,p)| - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
(|(p,p)| - (2 * |(p,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
((|.p.| ^2) - (2 * |(p,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
|.(p + p).| is V11() real ext-real non negative M2( REAL )
|.(p + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p + p).|,|.(p + p).|) is V11() real ext-real non negative set
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
|.(p - p).| is V11() real ext-real non negative M2( REAL )
|.(p - p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p - p).|,|.(p - p).|) is V11() real ext-real non negative set
(|.(p + p).| ^2) + (|.(p - p).| ^2) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
(|.p.| ^2) + (|.p.| ^2) is V11() real ext-real M2( REAL )
2 * ((|.p.| ^2) + (|.p.| ^2)) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
2 * |(p,p)| is V11() real ext-real M2( REAL )
(|.p.| ^2) - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
((|.p.| ^2) - (2 * |(p,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
((|.p.| ^2) + (|.p.| ^2)) - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
(|.p.| ^2) + (2 * |(p,p)|) is V11() real ext-real M2( REAL )
((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2)) + (|.(p - p).| ^2) is V11() real ext-real M2( REAL )
((|.p.| ^2) + (|.p.| ^2)) + (2 * |(p,p)|) is V11() real ext-real M2( REAL )
(((|.p.| ^2) + (|.p.| ^2)) + (2 * |(p,p)|)) + (((|.p.| ^2) + (|.p.| ^2)) - (2 * |(p,p)|)) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
|.(p + p).| is V11() real ext-real non negative M2( REAL )
|.(p + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p + p).|,|.(p + p).|) is V11() real ext-real non negative set
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
|.(p - p).| is V11() real ext-real non negative M2( REAL )
|.(p - p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p - p).|,|.(p - p).|) is V11() real ext-real non negative set
(|.(p + p).| ^2) - (|.(p - p).| ^2) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
4 * |(p,p)| is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
2 * |(p,p)| is V11() real ext-real M2( REAL )
(|.p.| ^2) + (2 * |(p,p)|) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2)) - (|.(p - p).| ^2) is V11() real ext-real M2( REAL )
(|.p.| ^2) - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
((|.p.| ^2) - (2 * |(p,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2)) - (((|.p.| ^2) - (2 * |(p,p)|)) + (|.p.| ^2)) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
|.(p + p).| is V11() real ext-real non negative M2( REAL )
|.(p + p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p + p).|,|.(p + p).|) is V11() real ext-real non negative set
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
|.(p - p).| is V11() real ext-real non negative M2( REAL )
|.(p - p).| ^2 is V11() real ext-real M2( REAL )
K37(|.(p - p).|,|.(p - p).|) is V11() real ext-real non negative set
(|.(p + p).| ^2) - (|.(p - p).| ^2) is V11() real ext-real M2( REAL )
(1 / 4) * ((|.(p + p).| ^2) - (|.(p - p).| ^2)) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
2 * |(p,p)| is V11() real ext-real M2( REAL )
(|.p.| ^2) + (2 * |(p,p)|) is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| ^2 is V11() real ext-real M2( REAL )
K37(|.p.|,|.p.|) is V11() real ext-real non negative set
((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2)) - (|.(p - p).| ^2) is V11() real ext-real M2( REAL )
(|.p.| ^2) - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
((|.p.| ^2) - (2 * |(p,p)|)) + (|.p.| ^2) is V11() real ext-real M2( REAL )
(((|.p.| ^2) + (2 * |(p,p)|)) + (|.p.| ^2)) - (((|.p.| ^2) - (2 * |(p,p)|)) + (|.p.| ^2)) is V11() real ext-real M2( REAL )
4 * |(p,p)| is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
|(p,p)| + |(p,p)| is V11() real ext-real M2( REAL )
0 + 0 is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
0 / 2 is V11() real ext-real V34() M2( RAT )
(|(p,p)| + |(p,p)|) / 2 is V11() real ext-real M2( REAL )
p - p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
- p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K163() is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K163() * p is V16() Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real set
K38(1) * p is V16() Function-like set
K369(K38(1)) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),K38(1),K83(REAL)) is set
K369(K38(1)) * p is V16() Function-like complex-valued ext-real-valued real-valued set
K259((TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,(- p)) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + (- p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,(- p)) is set
p - p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K250(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K166(),p,p) is set
K325(p) is V16() Function-like complex-valued set
K296(p,K325(p)) is V16() Function-like set
|((p - p),(p - p))| is V11() real ext-real M2( REAL )
mlt ((p - p),(p - p)) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p - p),(p - p)) is set
Sum (mlt ((p - p),(p - p))) is V11() real ext-real M2( REAL )
2 * |(p,p)| is V11() real ext-real M2( REAL )
|(p,p)| - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
(|(p,p)| - (2 * |(p,p)|)) + |(p,p)| is V11() real ext-real M2( REAL )
(|(p,p)| + |(p,p)|) - (2 * |(p,p)|) is V11() real ext-real M2( REAL )
(|(p,p)| + |(p,p)|) - 0 is V11() real ext-real M2( REAL )
(2 * |(p,p)|) / 2 is V11() real ext-real M2( REAL )
0 + |(p,p)| is V11() real ext-real M2( REAL )
((|(p,p)| + |(p,p)|) / 2) + ((|(p,p)| + |(p,p)|) / 2) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
abs |(p,p)| is V11() real ext-real M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| * |.p.| is V11() real ext-real non negative M2( REAL )
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|.p.| is V11() real ext-real non negative M2( REAL )
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
the U5 of (TOP-REAL n) is V16() V19(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n))) V20( the U1 of (TOP-REAL n)) Function-like V30(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) M2(K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))))
K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)) is set
K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n)) is set
K6(K7(K7( the U1 of (TOP-REAL n), the U1 of (TOP-REAL n)), the U1 of (TOP-REAL n))) is set
K418( the U1 of (TOP-REAL n), the U5 of (TOP-REAL n),p,p) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p + p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K165(),p,p) is set
|.(p + p).| is V11() real ext-real non negative M2( REAL )
|.p.| is V11() real ext-real non negative M2( REAL )
|.p.| + |.p.| is V11() real ext-real non negative M2( REAL )
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
len p is natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() M3( REAL , NAT )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,(0. (TOP-REAL n)))| is V11() real ext-real M2( REAL )
mlt (p,(0. (TOP-REAL n))) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,(0. (TOP-REAL n))) is set
Sum (mlt (p,(0. (TOP-REAL n)))) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,p)| is V11() real ext-real M2( REAL )
mlt (p,p) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K203(K167(),p,p) is set
Sum (mlt (p,p)) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V11() real ext-real set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p * p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p * p is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K369(p) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),p,K83(REAL)) is set
K369(p) * p is V16() Function-like complex-valued ext-real-valued real-valued set
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
|(p,q)| is V11() real ext-real M2( REAL )
mlt (p,q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),p,q) is set
Sum (mlt (p,q)) is V11() real ext-real M2( REAL )
p * |(p,q)| is V11() real ext-real M2( REAL )
|((p * p),q)| is V11() real ext-real M2( REAL )
mlt ((p * p),q) is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K203(K167(),(p * p),q) is set
Sum (mlt ((p * p),q)) is V11() real ext-real M2( REAL )
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V11() real ext-real set
p * q is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p * q is V16() V19( NAT ) V20( REAL ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K369(p) is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V30(K7(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued V170( REAL ) V171( REAL ) M2(K6(K7(K7(REAL,REAL),REAL)))
K83(REAL) is V1() V16() V19( REAL ) V20( REAL ) Function-like one-to-one V26( REAL ) complex-valued ext-real-valued real-valued M2(K6(K7(REAL,REAL)))
K205(K167(),p,K83(REAL)) is set
K369(p) * q is V16() Function-like complex-valued ext-real-valued real-valued set
n is natural V11() real ext-real set
TOP-REAL n is V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the U1 of (TOP-REAL n) is set
0. (TOP-REAL n) is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))
p is V16() V19( NAT ) Function-like V37() V44(n) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M2( the U1 of (TOP-REAL n))