REAL is V1() V34() V129() V130() V131() V135() set
NAT is V129() V130() V131() V132() V133() V134() V135() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V34() V129() V135() set
RAT is V1() V34() V129() V130() V131() V132() V135() set
INT is V1() V34() V129() V130() V131() V132() V133() V135() set
K7(COMPLEX,COMPLEX) is complex-yielding set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-yielding set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is complex-yielding V120() V121() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-yielding V120() V121() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V17( RAT ) complex-yielding V120() V121() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V17( RAT ) complex-yielding V120() V121() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V17( RAT ) V17( INT ) complex-yielding V120() V121() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V17( RAT ) V17( INT ) complex-yielding V120() V121() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V17( RAT ) V17( INT ) complex-yielding V120() V121() V122() set
K7(K7(NAT,NAT),NAT) is V17( RAT ) V17( INT ) complex-yielding V120() V121() V122() 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
K374() is V47() V75() L8()
the carrier of K374() is set
K379() is V47() V75() V97() V98() V99() V101() V151() V152() V153() V154() V155() V156() L8()
K380() is V47() V75() V99() V101() V154() V155() V156() M13(K379())
K381() is V47() V75() V97() V99() V101() V154() V155() V156() V157() M16(K379(),K380())
K383() is V47() V75() V97() V99() V101() L8()
K384() is V47() V75() V97() V99() V101() V157() M13(K383())
1 is V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() Element of NAT
K7(1,1) is V17( RAT ) V17( INT ) complex-yielding V120() V121() V122() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V17( RAT ) V17( INT ) complex-yielding V120() V121() V122() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-yielding V120() V121() set
K6(K7(K7(1,1),REAL)) is set
2 is V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() Element of NAT
K7(2,2) is V17( RAT ) V17( INT ) complex-yielding V120() V121() V122() set
K7(K7(2,2),REAL) is complex-yielding V120() V121() set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the carrier of (TOP-REAL 2) is set
0 is natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() Element of NAT
- 1 is V11() real V116() Element of REAL
multreal is V13() V16(K7(REAL,REAL)) V17( REAL ) Function-like V27(K7(REAL,REAL), REAL ) complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
3 is V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() Element of NAT
TOP-REAL 3 is V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() L16()
the carrier of (TOP-REAL 3) is set
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
REAL 3 is V1() functional FinSequence-membered FinSequenceSet of REAL
3 -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
p2 is V13() V16( NAT ) V17( REAL ) Function-like V41(3) FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p3 is V11() real V116() Element of REAL
x2 is V11() real V116() Element of REAL
y1 is V11() real V116() Element of REAL
<*p3,x2,y1*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 . 1 is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
p1 is V11() real V116() set
p2 is V11() real V116() set
p3 is V11() real V116() set
<*p1,p2,p3*> is set
x2 is V11() real V116() Element of REAL
y1 is V11() real V116() Element of REAL
y2 is V11() real V116() Element of REAL
<*x2,y1,y2*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
3 -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
REAL 3 is V1() functional FinSequence-membered FinSequenceSet of REAL
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
(p1,p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 1 is V11() real V116() Element of REAL
x2 is V11() real V116() Element of REAL
y1 is V11() real V116() Element of REAL
y2 is V11() real V116() Element of REAL
(x2,y1,y2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 2 is V11() real V116() Element of REAL
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
c9 is V11() real V116() Element of REAL
(p1,p2,c9) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p2,c9)) is V11() real V116() Element of REAL
(p1,p2,c9) . 3 is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
((p1),(p1),(p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
x2 is V11() real V116() Element of REAL
<*p2,p3,x2*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
0. (TOP-REAL 3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(0,0,0) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0* 3 is V13() V16( NAT ) V17( REAL ) Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of REAL 3
REAL 3 is V1() functional FinSequence-membered FinSequenceSet of REAL
3 |-> 0 is V13() empty-yielding V16( NAT ) V17( REAL ) Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of 3 -tuples_on REAL
3 -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
<*0,0,0*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 + p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) is V13() V16(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3))) V17( the carrier of (TOP-REAL 3)) Function-like V27(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) Element of K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)))
K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)) is set
K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) is set
K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3))) is set
the U5 of (TOP-REAL 3) . (p1,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 + p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1) + (p2) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) + (p2) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1) + (p2) is V11() real V116() Element of REAL
(((p1) + (p2)),((p1) + (p2)),((p1) + (p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
REAL 3 is V1() functional FinSequence-membered FinSequenceSet of REAL
p3 is V13() V16( NAT ) V17( REAL ) Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of REAL 3
x2 is V13() V16( NAT ) V17( REAL ) Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of REAL 3
p3 + x2 is V13() V16( NAT ) V17( REAL ) Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of REAL 3
len (p3 + x2) is natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() Element of NAT
dom (p3 + x2) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Seg 3 is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
(p3 + x2) . 2 is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
x2 . 2 is V11() real V116() Element of REAL
(p3 . 2) + (x2 . 2) is V11() real V116() Element of REAL
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 2 is V11() real V116() Element of REAL
(p3 + x2) . 3 is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
x2 . 3 is V11() real V116() Element of REAL
(p3 . 3) + (x2 . 3) is V11() real V116() Element of REAL
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 3 is V11() real V116() Element of REAL
(p3 + x2) . 1 is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
x2 . 1 is V11() real V116() Element of REAL
(p3 . 1) + (x2 . 1) is V11() real V116() Element of REAL
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 1 is V11() real V116() Element of REAL
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
(p1,p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
x2 is V11() real V116() Element of REAL
p1 + x2 is V11() real V116() Element of REAL
y1 is V11() real V116() Element of REAL
p2 + y1 is V11() real V116() Element of REAL
y2 is V11() real V116() Element of REAL
(x2,y1,y2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2,p3) + (x2,y1,y2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) is V13() V16(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3))) V17( the carrier of (TOP-REAL 3)) Function-like V27(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) Element of K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)))
K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)) is set
K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) is set
K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3))) is set
the U5 of (TOP-REAL 3) . ((p1,p2,p3),(x2,y1,y2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2,p3) + (x2,y1,y2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p3 + y2 is V11() real V116() Element of REAL
((p1 + x2),(p2 + y1),(p3 + y2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 3 is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 1 is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 2 is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 3 is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 1 is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 2 is V11() real V116() Element of REAL
p1 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
p1 * (p2) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
p1 * (p2) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
p1 * (p2) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
REAL 3 is V1() functional FinSequence-membered FinSequenceSet of REAL
p3 is V13() V16( NAT ) V17( REAL ) Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of REAL 3
p1 * p3 is V13() V16( NAT ) V17( REAL ) Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of REAL 3
(p1 * p3) . 2 is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
p1 * (p3 . 2) is V11() real V116() Element of REAL
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 2 is V11() real V116() Element of REAL
(p1 * p3) . 3 is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
p1 * (p3 . 3) is V11() real V116() Element of REAL
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 3 is V11() real V116() Element of REAL
(p1 * p3) . 1 is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
p1 * (p3 . 1) is V11() real V116() Element of REAL
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 1 is V11() real V116() Element of REAL
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
p1 * p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
p1 * p3 is V11() real V116() Element of REAL
x2 is V11() real V116() Element of REAL
(p2,p3,x2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * (p2,p3,x2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * (p2,p3,x2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 * x2 is V11() real V116() Element of REAL
((p1 * p2),(p1 * p3),(p1 * x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p2,p3,x2)) is V11() real V116() Element of REAL
(p2,p3,x2) . 3 is V11() real V116() Element of REAL
((p2,p3,x2)) is V11() real V116() Element of REAL
(p2,p3,x2) . 1 is V11() real V116() Element of REAL
((p2,p3,x2)) is V11() real V116() Element of REAL
(p2,p3,x2) . 2 is V11() real V116() Element of REAL
p1 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 1 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
p1 * (p2) is V11() real V116() Element of REAL
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 2 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
p1 * (p2) is V11() real V116() Element of REAL
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
p1 * (p2) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) . 3 is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) . 1 is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) . 2 is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- p1 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
- (p1) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
- (p1) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
- (p1) is V11() real V116() Element of REAL
((- (p1)),(- (p1)),(- (p1))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(- 1) * p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(- 1) * p1 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(- 1) * (p1) is V11() real V116() Element of REAL
(- 1) * (p1) is V11() real V116() Element of REAL
(- 1) * (p1) is V11() real V116() Element of REAL
(((- 1) * (p1)),((- 1) * (p1)),((- 1) * (p1))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V11() real V116() Element of REAL
- p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
- p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
(p1,p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p1,p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p1,p2,p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
- p3 is V11() real V116() Element of REAL
((- p1),(- p2),(- p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 3 is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 1 is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 2 is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 - p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K237((TOP-REAL 3),p1,(- p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) is V13() V16(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3))) V17( the carrier of (TOP-REAL 3)) Function-like V27(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) Element of K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)))
K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)) is set
K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) is set
K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3))) is set
the U5 of (TOP-REAL 3) . (p1,(- p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 + (- p2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 - p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1) - (p2) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) - (p2) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1) - (p2) is V11() real V116() Element of REAL
(((p1) - (p2)),((p1) - (p2)),((p1) - (p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p2) is V11() real V116() Element of REAL
- (p2) is V11() real V116() Element of REAL
- (p2) is V11() real V116() Element of REAL
((- (p2)),(- (p2)),(- (p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((- p2)) is V11() real V116() Element of REAL
(- p2) . 3 is V11() real V116() Element of REAL
((- p2)) is V11() real V116() Element of REAL
(- p2) . 1 is V11() real V116() Element of REAL
((- p2)) is V11() real V116() Element of REAL
(- p2) . 2 is V11() real V116() Element of REAL
(p1) + (- (p2)) is V11() real V116() Element of REAL
(p1) + (- (p2)) is V11() real V116() Element of REAL
(p1) + (- (p2)) is V11() real V116() Element of REAL
(((p1) + (- (p2))),((p1) + (- (p2))),((p1) + (- (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
(p1,p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
x2 is V11() real V116() Element of REAL
p1 - x2 is V11() real V116() Element of REAL
y1 is V11() real V116() Element of REAL
p2 - y1 is V11() real V116() Element of REAL
y2 is V11() real V116() Element of REAL
(x2,y1,y2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2,p3) - (x2,y1,y2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (x2,y1,y2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (x2,y1,y2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K237((TOP-REAL 3),(p1,p2,p3),(- (x2,y1,y2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) is V13() V16(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3))) V17( the carrier of (TOP-REAL 3)) Function-like V27(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) Element of K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)))
K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)) is set
K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) is set
K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3))) is set
the U5 of (TOP-REAL 3) . ((p1,p2,p3),(- (x2,y1,y2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2,p3) + (- (x2,y1,y2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1,p2,p3) - (x2,y1,y2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p3 - y2 is V11() real V116() Element of REAL
((p1 - x2),(p2 - y1),(p3 - y2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 3 is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 1 is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 2 is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 3 is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 1 is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 2 is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
x2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
(p1,p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(x2) is V11() real V116() Element of REAL
x2 . 1 is V11() real V116() Element of REAL
(x2) is V11() real V116() Element of REAL
x2 . 2 is V11() real V116() Element of REAL
(x2) is V11() real V116() Element of REAL
x2 . 3 is V11() real V116() Element of REAL
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
(p1,p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
x2 is V11() real V116() Element of REAL
p3 * x2 is V11() real V116() Element of REAL
p2 * x2 is V11() real V116() Element of REAL
y1 is V11() real V116() Element of REAL
p3 * y1 is V11() real V116() Element of REAL
p1 * y1 is V11() real V116() Element of REAL
(p1 * y1) - (p2 * x2) is V11() real V116() Element of REAL
y2 is V11() real V116() Element of REAL
(x2,y1,y2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p2,p3),(x2,y1,y2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 2 is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 3 is V11() real V116() Element of REAL
((p1,p2,p3)) * ((x2,y1,y2)) is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 3 is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 2 is V11() real V116() Element of REAL
((p1,p2,p3)) * ((x2,y1,y2)) is V11() real V116() Element of REAL
(((p1,p2,p3)) * ((x2,y1,y2))) - (((p1,p2,p3)) * ((x2,y1,y2))) is V11() real V116() Element of REAL
((x2,y1,y2)) is V11() real V116() Element of REAL
(x2,y1,y2) . 1 is V11() real V116() Element of REAL
((p1,p2,p3)) * ((x2,y1,y2)) is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 1 is V11() real V116() Element of REAL
((p1,p2,p3)) * ((x2,y1,y2)) is V11() real V116() Element of REAL
(((p1,p2,p3)) * ((x2,y1,y2))) - (((p1,p2,p3)) * ((x2,y1,y2))) is V11() real V116() Element of REAL
((p1,p2,p3)) * ((x2,y1,y2)) is V11() real V116() Element of REAL
((p1,p2,p3)) * ((x2,y1,y2)) is V11() real V116() Element of REAL
(((p1,p2,p3)) * ((x2,y1,y2))) - (((p1,p2,p3)) * ((x2,y1,y2))) is V11() real V116() Element of REAL
(((((p1,p2,p3)) * ((x2,y1,y2))) - (((p1,p2,p3)) * ((x2,y1,y2)))),((((p1,p2,p3)) * ((x2,y1,y2))) - (((p1,p2,p3)) * ((x2,y1,y2)))),((((p1,p2,p3)) * ((x2,y1,y2))) - (((p1,p2,p3)) * ((x2,y1,y2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 * y2 is V11() real V116() Element of REAL
(p2 * y2) - (p3 * y1) is V11() real V116() Element of REAL
p1 * y2 is V11() real V116() Element of REAL
(p3 * x2) - (p1 * y2) is V11() real V116() Element of REAL
(((p2 * y2) - (p3 * y1)),((p3 * x2) - (p1 * y2)),((p1 * y1) - (p2 * x2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
p1 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1 * p2),p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 2 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
((p1 * p2)) * (p3) is V11() real V116() Element of REAL
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 3 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
((p1 * p2)) * (p3) is V11() real V116() Element of REAL
(((p1 * p2)) * (p3)) - (((p1 * p2)) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
((p1 * p2)) * (p3) is V11() real V116() Element of REAL
((p1 * p2)) is V11() real V116() Element of REAL
(p1 * p2) . 1 is V11() real V116() Element of REAL
((p1 * p2)) * (p3) is V11() real V116() Element of REAL
(((p1 * p2)) * (p3)) - (((p1 * p2)) * (p3)) is V11() real V116() Element of REAL
((p1 * p2)) * (p3) is V11() real V116() Element of REAL
((p1 * p2)) * (p3) is V11() real V116() Element of REAL
(((p1 * p2)) * (p3)) - (((p1 * p2)) * (p3)) is V11() real V116() Element of REAL
(((((p1 * p2)) * (p3)) - (((p1 * p2)) * (p3))),((((p1 * p2)) * (p3)) - (((p1 * p2)) * (p3))),((((p1 * p2)) * (p3)) - (((p1 * p2)) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * (p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * (p2,p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 * p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * p3 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p2,(p1 * p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1 * p3)) is V11() real V116() Element of REAL
(p1 * p3) . 3 is V11() real V116() Element of REAL
(p2) * ((p1 * p3)) is V11() real V116() Element of REAL
((p1 * p3)) is V11() real V116() Element of REAL
(p1 * p3) . 2 is V11() real V116() Element of REAL
(p2) * ((p1 * p3)) is V11() real V116() Element of REAL
((p2) * ((p1 * p3))) - ((p2) * ((p1 * p3))) is V11() real V116() Element of REAL
((p1 * p3)) is V11() real V116() Element of REAL
(p1 * p3) . 1 is V11() real V116() Element of REAL
(p2) * ((p1 * p3)) is V11() real V116() Element of REAL
(p2) * ((p1 * p3)) is V11() real V116() Element of REAL
((p2) * ((p1 * p3))) - ((p2) * ((p1 * p3))) is V11() real V116() Element of REAL
(p2) * ((p1 * p3)) is V11() real V116() Element of REAL
(p2) * ((p1 * p3)) is V11() real V116() Element of REAL
((p2) * ((p1 * p3))) - ((p2) * ((p1 * p3))) is V11() real V116() Element of REAL
((((p2) * ((p1 * p3))) - ((p2) * ((p1 * p3)))),(((p2) * ((p1 * p3))) - ((p2) * ((p1 * p3)))),(((p2) * ((p1 * p3))) - ((p2) * ((p1 * p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * (p2) is V11() real V116() Element of REAL
p1 * (p2) is V11() real V116() Element of REAL
p1 * (p2) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2))),p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) . 2 is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3) is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) . 3 is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3) is V11() real V116() Element of REAL
((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3) is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) is V11() real V116() Element of REAL
((p1 * (p2)),(p1 * (p2)),(p1 * (p2))) . 1 is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3) is V11() real V116() Element of REAL
((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3) is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3) is V11() real V116() Element of REAL
((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) is V11() real V116() Element of REAL
((((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3))),(((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3))),(((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p3),(p3),(p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2))),((p3),(p3),(p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p3),(p3),(p3))) is V11() real V116() Element of REAL
((p3),(p3),(p3)) . 3 is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3))) is V11() real V116() Element of REAL
(((p3),(p3),(p3))) is V11() real V116() Element of REAL
((p3),(p3),(p3)) . 2 is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3))) is V11() real V116() Element of REAL
((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) is V11() real V116() Element of REAL
(((p3),(p3),(p3))) is V11() real V116() Element of REAL
((p3),(p3),(p3)) . 1 is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3))) is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3))) is V11() real V116() Element of REAL
((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3))) is V11() real V116() Element of REAL
(((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3))) is V11() real V116() Element of REAL
((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) is V11() real V116() Element of REAL
((((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3))))),(((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3))))),(((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))) - ((((p1 * (p2)),(p1 * (p2)),(p1 * (p2)))) * (((p3),(p3),(p3)))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1 * (p2)) * (p3) is V11() real V116() Element of REAL
(p1 * (p2)) * (p3) is V11() real V116() Element of REAL
((p1 * (p2)) * (p3)) - ((p1 * (p2)) * (p3)) is V11() real V116() Element of REAL
(p1 * (p2)) * (p3) is V11() real V116() Element of REAL
(p1 * (p2)) * (p3) is V11() real V116() Element of REAL
((p1 * (p2)) * (p3)) - ((p1 * (p2)) * (p3)) is V11() real V116() Element of REAL
(p1 * (p2)) * (p3) is V11() real V116() Element of REAL
(p1 * (p2)) * (p3) is V11() real V116() Element of REAL
((p1 * (p2)) * (p3)) - ((p1 * (p2)) * (p3)) is V11() real V116() Element of REAL
((((p1 * (p2)) * (p3)) - ((p1 * (p2)) * (p3))),(((p1 * (p2)) * (p3)) - ((p1 * (p2)) * (p3))),(((p1 * (p2)) * (p3)) - ((p1 * (p2)) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
p1 * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
p1 * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
((p1 * (((p2) * (p3)) - ((p2) * (p3)))),(p1 * (((p2) * (p3)) - ((p2) * (p3)))),(p1 * (((p2) * (p3)) - ((p2) * (p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * (p3) is V11() real V116() Element of REAL
(p2) * (p1 * (p3)) is V11() real V116() Element of REAL
p1 * (p3) is V11() real V116() Element of REAL
(p2) * (p1 * (p3)) is V11() real V116() Element of REAL
((p2) * (p1 * (p3))) - ((p2) * (p1 * (p3))) is V11() real V116() Element of REAL
p1 * (p3) is V11() real V116() Element of REAL
(p2) * (p1 * (p3)) is V11() real V116() Element of REAL
(p2) * (p1 * (p3)) is V11() real V116() Element of REAL
((p2) * (p1 * (p3))) - ((p2) * (p1 * (p3))) is V11() real V116() Element of REAL
(p2) * (p1 * (p3)) is V11() real V116() Element of REAL
(p2) * (p1 * (p3)) is V11() real V116() Element of REAL
((p2) * (p1 * (p3))) - ((p2) * (p1 * (p3))) is V11() real V116() Element of REAL
((((p2) * (p1 * (p3))) - ((p2) * (p1 * (p3)))),(((p2) * (p1 * (p3))) - ((p2) * (p1 * (p3)))),(((p2) * (p1 * (p3))) - ((p2) * (p1 * (p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p2),(p2),(p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1 * (p3)),(p1 * (p3)),(p1 * (p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p2),(p2),(p2)),((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p2),(p2),(p2))) is V11() real V116() Element of REAL
((p2),(p2),(p2)) . 2 is V11() real V116() Element of REAL
(((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((p1 * (p3)),(p1 * (p3)),(p1 * (p3))) . 3 is V11() real V116() Element of REAL
(((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
(((p2),(p2),(p2))) is V11() real V116() Element of REAL
((p2),(p2),(p2)) . 3 is V11() real V116() Element of REAL
(((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((p1 * (p3)),(p1 * (p3)),(p1 * (p3))) . 2 is V11() real V116() Element of REAL
(((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) is V11() real V116() Element of REAL
(((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((p1 * (p3)),(p1 * (p3)),(p1 * (p3))) . 1 is V11() real V116() Element of REAL
(((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
(((p2),(p2),(p2))) is V11() real V116() Element of REAL
((p2),(p2),(p2)) . 1 is V11() real V116() Element of REAL
(((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) is V11() real V116() Element of REAL
(((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
(((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) is V11() real V116() Element of REAL
((((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))))),(((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))))),(((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((((p2),(p2),(p2))) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
(p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) is V11() real V116() Element of REAL
(p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
(p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) is V11() real V116() Element of REAL
(p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
(p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))) is V11() real V116() Element of REAL
((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) is V11() real V116() Element of REAL
((((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))))),(((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3)))))),(((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))) - ((p2) * (((p1 * (p3)),(p1 * (p3)),(p1 * (p3))))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) * (p1) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
((p2) * (p1)) - ((p2) * (p1)) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
((p2) * (p1)) - ((p2) * (p1)) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
((p2) * (p1)) - ((p2) * (p1)) is V11() real V116() Element of REAL
((((p2) * (p1)) - ((p2) * (p1))),(((p2) * (p1)) - ((p2) * (p1))),(((p2) * (p1)) - ((p2) * (p1)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p2,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p2,p1) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(- 1) * (p2,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(- 1) * (p2,p1) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(- 1) * (((p2) * (p1)) - ((p2) * (p1))) is V11() real V116() Element of REAL
(- 1) * (((p2) * (p1)) - ((p2) * (p1))) is V11() real V116() Element of REAL
(- 1) * (((p2) * (p1)) - ((p2) * (p1))) is V11() real V116() Element of REAL
(((- 1) * (((p2) * (p1)) - ((p2) * (p1)))),((- 1) * (((p2) * (p1)) - ((p2) * (p1)))),((- 1) * (((p2) * (p1)) - ((p2) * (p1))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- p1 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((- p1),p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((- p1)) is V11() real V116() Element of REAL
(- p1) . 2 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
((- p1)) * (p2) is V11() real V116() Element of REAL
((- p1)) is V11() real V116() Element of REAL
(- p1) . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
((- p1)) * (p2) is V11() real V116() Element of REAL
(((- p1)) * (p2)) - (((- p1)) * (p2)) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
((- p1)) * (p2) is V11() real V116() Element of REAL
((- p1)) is V11() real V116() Element of REAL
(- p1) . 1 is V11() real V116() Element of REAL
((- p1)) * (p2) is V11() real V116() Element of REAL
(((- p1)) * (p2)) - (((- p1)) * (p2)) is V11() real V116() Element of REAL
((- p1)) * (p2) is V11() real V116() Element of REAL
((- p1)) * (p2) is V11() real V116() Element of REAL
(((- p1)) * (p2)) - (((- p1)) * (p2)) is V11() real V116() Element of REAL
(((((- p1)) * (p2)) - (((- p1)) * (p2))),((((- p1)) * (p2)) - (((- p1)) * (p2))),((((- p1)) * (p2)) - (((- p1)) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1,(- p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
((- p2)) is V11() real V116() Element of REAL
(- p2) . 3 is V11() real V116() Element of REAL
(p1) * ((- p2)) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
((- p2)) is V11() real V116() Element of REAL
(- p2) . 2 is V11() real V116() Element of REAL
(p1) * ((- p2)) is V11() real V116() Element of REAL
((p1) * ((- p2))) - ((p1) * ((- p2))) is V11() real V116() Element of REAL
((- p2)) is V11() real V116() Element of REAL
(- p2) . 1 is V11() real V116() Element of REAL
(p1) * ((- p2)) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * ((- p2)) is V11() real V116() Element of REAL
((p1) * ((- p2))) - ((p1) * ((- p2))) is V11() real V116() Element of REAL
(p1) * ((- p2)) is V11() real V116() Element of REAL
(p1) * ((- p2)) is V11() real V116() Element of REAL
((p1) * ((- p2))) - ((p1) * ((- p2))) is V11() real V116() Element of REAL
((((p1) * ((- p2))) - ((p1) * ((- p2)))),(((p1) * ((- p2))) - ((p1) * ((- p2)))),(((p1) * ((- p2))) - ((p1) * ((- p2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p1) is V11() real V116() Element of REAL
- (p1) is V11() real V116() Element of REAL
- (p1) is V11() real V116() Element of REAL
((- (p1)),(- (p1)),(- (p1))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((- (p1)),(- (p1)),(- (p1))),p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((- (p1)),(- (p1)),(- (p1)))) is V11() real V116() Element of REAL
((- (p1)),(- (p1)),(- (p1))) . 2 is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (p2) is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) is V11() real V116() Element of REAL
((- (p1)),(- (p1)),(- (p1))) . 3 is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (p2) is V11() real V116() Element of REAL
((((- (p1)),(- (p1)),(- (p1)))) * (p2)) - ((((- (p1)),(- (p1)),(- (p1)))) * (p2)) is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (p2) is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) is V11() real V116() Element of REAL
((- (p1)),(- (p1)),(- (p1))) . 1 is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (p2) is V11() real V116() Element of REAL
((((- (p1)),(- (p1)),(- (p1)))) * (p2)) - ((((- (p1)),(- (p1)),(- (p1)))) * (p2)) is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (p2) is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (p2) is V11() real V116() Element of REAL
((((- (p1)),(- (p1)),(- (p1)))) * (p2)) - ((((- (p1)),(- (p1)),(- (p1)))) * (p2)) is V11() real V116() Element of REAL
((((((- (p1)),(- (p1)),(- (p1)))) * (p2)) - ((((- (p1)),(- (p1)),(- (p1)))) * (p2))),(((((- (p1)),(- (p1)),(- (p1)))) * (p2)) - ((((- (p1)),(- (p1)),(- (p1)))) * (p2))),(((((- (p1)),(- (p1)),(- (p1)))) * (p2)) - ((((- (p1)),(- (p1)),(- (p1)))) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p2),(p2),(p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((- (p1)),(- (p1)),(- (p1))),((p2),(p2),(p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p2),(p2),(p2))) is V11() real V116() Element of REAL
((p2),(p2),(p2)) . 3 is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2))) is V11() real V116() Element of REAL
(((p2),(p2),(p2))) is V11() real V116() Element of REAL
((p2),(p2),(p2)) . 2 is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2))) is V11() real V116() Element of REAL
((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) - ((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) is V11() real V116() Element of REAL
(((p2),(p2),(p2))) is V11() real V116() Element of REAL
((p2),(p2),(p2)) . 1 is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2))) is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2))) is V11() real V116() Element of REAL
((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) - ((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2))) is V11() real V116() Element of REAL
(((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2))) is V11() real V116() Element of REAL
((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) - ((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) is V11() real V116() Element of REAL
((((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) - ((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2))))),(((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) - ((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2))))),(((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))) - ((((- (p1)),(- (p1)),(- (p1)))) * (((p2),(p2),(p2)))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(- (p1)) * (p2) is V11() real V116() Element of REAL
(- (p1)) * (p2) is V11() real V116() Element of REAL
((- (p1)) * (p2)) - ((- (p1)) * (p2)) is V11() real V116() Element of REAL
(- (p1)) * (p2) is V11() real V116() Element of REAL
(- (p1)) * (p2) is V11() real V116() Element of REAL
((- (p1)) * (p2)) - ((- (p1)) * (p2)) is V11() real V116() Element of REAL
(- (p1)) * (p2) is V11() real V116() Element of REAL
(- (p1)) * (p2) is V11() real V116() Element of REAL
((- (p1)) * (p2)) - ((- (p1)) * (p2)) is V11() real V116() Element of REAL
((((- (p1)) * (p2)) - ((- (p1)) * (p2))),(((- (p1)) * (p2)) - ((- (p1)) * (p2))),(((- (p1)) * (p2)) - ((- (p1)) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p2) is V11() real V116() Element of REAL
(p1) * (- (p2)) is V11() real V116() Element of REAL
- (p2) is V11() real V116() Element of REAL
(p1) * (- (p2)) is V11() real V116() Element of REAL
((p1) * (- (p2))) - ((p1) * (- (p2))) is V11() real V116() Element of REAL
- (p2) is V11() real V116() Element of REAL
(p1) * (- (p2)) is V11() real V116() Element of REAL
(p1) * (- (p2)) is V11() real V116() Element of REAL
((p1) * (- (p2))) - ((p1) * (- (p2))) is V11() real V116() Element of REAL
(p1) * (- (p2)) is V11() real V116() Element of REAL
(p1) * (- (p2)) is V11() real V116() Element of REAL
((p1) * (- (p2))) - ((p1) * (- (p2))) is V11() real V116() Element of REAL
((((p1) * (- (p2))) - ((p1) * (- (p2)))),(((p1) * (- (p2))) - ((p1) * (- (p2)))),(((p1) * (- (p2))) - ((p1) * (- (p2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1),(p1),(p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((- (p2)),(- (p2)),(- (p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1),(p1),(p1)),((- (p2)),(- (p2)),(- (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1),(p1),(p1))) is V11() real V116() Element of REAL
((p1),(p1),(p1)) . 2 is V11() real V116() Element of REAL
(((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
((- (p2)),(- (p2)),(- (p2))) . 3 is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) is V11() real V116() Element of REAL
((p1),(p1),(p1)) . 3 is V11() real V116() Element of REAL
(((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
((- (p2)),(- (p2)),(- (p2))) . 2 is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) - ((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) is V11() real V116() Element of REAL
(((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
((- (p2)),(- (p2)),(- (p2))) . 1 is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) is V11() real V116() Element of REAL
((p1),(p1),(p1)) . 1 is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) - ((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2)))) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) - ((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) is V11() real V116() Element of REAL
((((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) - ((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2)))))),(((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) - ((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2)))))),(((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))) - ((((p1),(p1),(p1))) * (((- (p2)),(- (p2)),(- (p2))))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1),(p1),(p1)),(- p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1),(p1),(p1))) * ((- p2)) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * ((- p2)) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * ((- p2))) - ((((p1),(p1),(p1))) * ((- p2))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * ((- p2)) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * ((- p2)) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * ((- p2))) - ((((p1),(p1),(p1))) * ((- p2))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * ((- p2)) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * ((- p2)) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * ((- p2))) - ((((p1),(p1),(p1))) * ((- p2))) is V11() real V116() Element of REAL
((((((p1),(p1),(p1))) * ((- p2))) - ((((p1),(p1),(p1))) * ((- p2)))),(((((p1),(p1),(p1))) * ((- p2))) - ((((p1),(p1),(p1))) * ((- p2)))),(((((p1),(p1),(p1))) * ((- p2))) - ((((p1),(p1),(p1))) * ((- p2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
(p1,p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((0,0,0),(p1,p2,p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((0,0,0)) is V11() real V116() Element of REAL
(0,0,0) . 2 is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 3 is V11() real V116() Element of REAL
((0,0,0)) * ((p1,p2,p3)) is V11() real V116() Element of REAL
((0,0,0)) is V11() real V116() Element of REAL
(0,0,0) . 3 is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 2 is V11() real V116() Element of REAL
((0,0,0)) * ((p1,p2,p3)) is V11() real V116() Element of REAL
(((0,0,0)) * ((p1,p2,p3))) - (((0,0,0)) * ((p1,p2,p3))) is V11() real V116() Element of REAL
((p1,p2,p3)) is V11() real V116() Element of REAL
(p1,p2,p3) . 1 is V11() real V116() Element of REAL
((0,0,0)) * ((p1,p2,p3)) is V11() real V116() Element of REAL
((0,0,0)) is V11() real V116() Element of REAL
(0,0,0) . 1 is V11() real V116() Element of REAL
((0,0,0)) * ((p1,p2,p3)) is V11() real V116() Element of REAL
(((0,0,0)) * ((p1,p2,p3))) - (((0,0,0)) * ((p1,p2,p3))) is V11() real V116() Element of REAL
((0,0,0)) * ((p1,p2,p3)) is V11() real V116() Element of REAL
((0,0,0)) * ((p1,p2,p3)) is V11() real V116() Element of REAL
(((0,0,0)) * ((p1,p2,p3))) - (((0,0,0)) * ((p1,p2,p3))) is V11() real V116() Element of REAL
(((((0,0,0)) * ((p1,p2,p3))) - (((0,0,0)) * ((p1,p2,p3)))),((((0,0,0)) * ((p1,p2,p3))) - (((0,0,0)) * ((p1,p2,p3)))),((((0,0,0)) * ((p1,p2,p3))) - (((0,0,0)) * ((p1,p2,p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * p3 is V11() real V116() Element of REAL
0 * p2 is V11() real V116() Element of REAL
(0 * p3) - (0 * p2) is V11() real V116() Element of REAL
0 * p1 is V11() real V116() Element of REAL
(0 * p1) - (0 * p3) is V11() real V116() Element of REAL
(0 * p2) - (0 * p1) is V11() real V116() Element of REAL
(((0 * p3) - (0 * p2)),((0 * p1) - (0 * p3)),((0 * p2) - (0 * p1))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p3 - p2 is V11() real V116() Element of REAL
0 * (p3 - p2) is V11() real V116() Element of REAL
p1 - p3 is V11() real V116() Element of REAL
0 * (p1 - p3) is V11() real V116() Element of REAL
p2 - p1 is V11() real V116() Element of REAL
0 * (p2 - p1) is V11() real V116() Element of REAL
((0 * (p3 - p2)),(0 * (p1 - p3)),(0 * (p2 - p1))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p3 - p2),(p1 - p3),(p2 - p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * ((p3 - p2),(p1 - p3),(p2 - p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * ((p3 - p2),(p1 - p3),(p2 - p1)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V11() real V116() Element of REAL
(p1,0,0) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V11() real V116() Element of REAL
(p2,0,0) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,0,0),(p2,0,0)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,0,0)) is V11() real V116() Element of REAL
(p1,0,0) . 2 is V11() real V116() Element of REAL
((p2,0,0)) is V11() real V116() Element of REAL
(p2,0,0) . 3 is V11() real V116() Element of REAL
((p1,0,0)) * ((p2,0,0)) is V11() real V116() Element of REAL
((p1,0,0)) is V11() real V116() Element of REAL
(p1,0,0) . 3 is V11() real V116() Element of REAL
((p2,0,0)) is V11() real V116() Element of REAL
(p2,0,0) . 2 is V11() real V116() Element of REAL
((p1,0,0)) * ((p2,0,0)) is V11() real V116() Element of REAL
(((p1,0,0)) * ((p2,0,0))) - (((p1,0,0)) * ((p2,0,0))) is V11() real V116() Element of REAL
((p2,0,0)) is V11() real V116() Element of REAL
(p2,0,0) . 1 is V11() real V116() Element of REAL
((p1,0,0)) * ((p2,0,0)) is V11() real V116() Element of REAL
((p1,0,0)) is V11() real V116() Element of REAL
(p1,0,0) . 1 is V11() real V116() Element of REAL
((p1,0,0)) * ((p2,0,0)) is V11() real V116() Element of REAL
(((p1,0,0)) * ((p2,0,0))) - (((p1,0,0)) * ((p2,0,0))) is V11() real V116() Element of REAL
((p1,0,0)) * ((p2,0,0)) is V11() real V116() Element of REAL
((p1,0,0)) * ((p2,0,0)) is V11() real V116() Element of REAL
(((p1,0,0)) * ((p2,0,0))) - (((p1,0,0)) * ((p2,0,0))) is V11() real V116() Element of REAL
(((((p1,0,0)) * ((p2,0,0))) - (((p1,0,0)) * ((p2,0,0)))),((((p1,0,0)) * ((p2,0,0))) - (((p1,0,0)) * ((p2,0,0)))),((((p1,0,0)) * ((p2,0,0))) - (((p1,0,0)) * ((p2,0,0))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * 0 is V11() real V116() Element of REAL
(0 * 0) - (0 * 0) is V11() real V116() Element of REAL
0 * p2 is V11() real V116() Element of REAL
p1 * 0 is V11() real V116() Element of REAL
(0 * p2) - (p1 * 0) is V11() real V116() Element of REAL
(p1 * 0) - (0 * p2) is V11() real V116() Element of REAL
(((0 * 0) - (0 * 0)),((0 * p2) - (p1 * 0)),((p1 * 0) - (0 * p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 - 0 is V11() real V116() Element of REAL
0 * (0 - 0) is V11() real V116() Element of REAL
p2 - p1 is V11() real V116() Element of REAL
0 * (p2 - p1) is V11() real V116() Element of REAL
p1 - p2 is V11() real V116() Element of REAL
0 * (p1 - p2) is V11() real V116() Element of REAL
((0 * (0 - 0)),(0 * (p2 - p1)),(0 * (p1 - p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((0 - 0),(p2 - p1),(p1 - p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * ((0 - 0),(p2 - p1),(p1 - p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * ((0 - 0),(p2 - p1),(p1 - p2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V11() real V116() Element of REAL
(0,p1,0) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V11() real V116() Element of REAL
(0,p2,0) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((0,p1,0),(0,p2,0)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((0,p1,0)) is V11() real V116() Element of REAL
(0,p1,0) . 2 is V11() real V116() Element of REAL
((0,p2,0)) is V11() real V116() Element of REAL
(0,p2,0) . 3 is V11() real V116() Element of REAL
((0,p1,0)) * ((0,p2,0)) is V11() real V116() Element of REAL
((0,p1,0)) is V11() real V116() Element of REAL
(0,p1,0) . 3 is V11() real V116() Element of REAL
((0,p2,0)) is V11() real V116() Element of REAL
(0,p2,0) . 2 is V11() real V116() Element of REAL
((0,p1,0)) * ((0,p2,0)) is V11() real V116() Element of REAL
(((0,p1,0)) * ((0,p2,0))) - (((0,p1,0)) * ((0,p2,0))) is V11() real V116() Element of REAL
((0,p2,0)) is V11() real V116() Element of REAL
(0,p2,0) . 1 is V11() real V116() Element of REAL
((0,p1,0)) * ((0,p2,0)) is V11() real V116() Element of REAL
((0,p1,0)) is V11() real V116() Element of REAL
(0,p1,0) . 1 is V11() real V116() Element of REAL
((0,p1,0)) * ((0,p2,0)) is V11() real V116() Element of REAL
(((0,p1,0)) * ((0,p2,0))) - (((0,p1,0)) * ((0,p2,0))) is V11() real V116() Element of REAL
((0,p1,0)) * ((0,p2,0)) is V11() real V116() Element of REAL
((0,p1,0)) * ((0,p2,0)) is V11() real V116() Element of REAL
(((0,p1,0)) * ((0,p2,0))) - (((0,p1,0)) * ((0,p2,0))) is V11() real V116() Element of REAL
(((((0,p1,0)) * ((0,p2,0))) - (((0,p1,0)) * ((0,p2,0)))),((((0,p1,0)) * ((0,p2,0))) - (((0,p1,0)) * ((0,p2,0)))),((((0,p1,0)) * ((0,p2,0))) - (((0,p1,0)) * ((0,p2,0))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 * 0 is V11() real V116() Element of REAL
0 * p2 is V11() real V116() Element of REAL
(p1 * 0) - (0 * p2) is V11() real V116() Element of REAL
0 * 0 is V11() real V116() Element of REAL
(0 * 0) - (0 * 0) is V11() real V116() Element of REAL
(0 * p2) - (p1 * 0) is V11() real V116() Element of REAL
(((p1 * 0) - (0 * p2)),((0 * 0) - (0 * 0)),((0 * p2) - (p1 * 0))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 - p2 is V11() real V116() Element of REAL
0 * (p1 - p2) is V11() real V116() Element of REAL
0 - 0 is V11() real V116() Element of REAL
0 * (0 - 0) is V11() real V116() Element of REAL
p2 - p1 is V11() real V116() Element of REAL
0 * (p2 - p1) is V11() real V116() Element of REAL
((0 * (p1 - p2)),(0 * (0 - 0)),(0 * (p2 - p1))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1 - p2),(0 - 0),(p2 - p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * ((p1 - p2),(0 - 0),(p2 - p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * ((p1 - p2),(0 - 0),(p2 - p1)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V11() real V116() Element of REAL
(0,0,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V11() real V116() Element of REAL
(0,0,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((0,0,p1),(0,0,p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((0,0,p1)) is V11() real V116() Element of REAL
(0,0,p1) . 2 is V11() real V116() Element of REAL
((0,0,p2)) is V11() real V116() Element of REAL
(0,0,p2) . 3 is V11() real V116() Element of REAL
((0,0,p1)) * ((0,0,p2)) is V11() real V116() Element of REAL
((0,0,p1)) is V11() real V116() Element of REAL
(0,0,p1) . 3 is V11() real V116() Element of REAL
((0,0,p2)) is V11() real V116() Element of REAL
(0,0,p2) . 2 is V11() real V116() Element of REAL
((0,0,p1)) * ((0,0,p2)) is V11() real V116() Element of REAL
(((0,0,p1)) * ((0,0,p2))) - (((0,0,p1)) * ((0,0,p2))) is V11() real V116() Element of REAL
((0,0,p2)) is V11() real V116() Element of REAL
(0,0,p2) . 1 is V11() real V116() Element of REAL
((0,0,p1)) * ((0,0,p2)) is V11() real V116() Element of REAL
((0,0,p1)) is V11() real V116() Element of REAL
(0,0,p1) . 1 is V11() real V116() Element of REAL
((0,0,p1)) * ((0,0,p2)) is V11() real V116() Element of REAL
(((0,0,p1)) * ((0,0,p2))) - (((0,0,p1)) * ((0,0,p2))) is V11() real V116() Element of REAL
((0,0,p1)) * ((0,0,p2)) is V11() real V116() Element of REAL
((0,0,p1)) * ((0,0,p2)) is V11() real V116() Element of REAL
(((0,0,p1)) * ((0,0,p2))) - (((0,0,p1)) * ((0,0,p2))) is V11() real V116() Element of REAL
(((((0,0,p1)) * ((0,0,p2))) - (((0,0,p1)) * ((0,0,p2)))),((((0,0,p1)) * ((0,0,p2))) - (((0,0,p1)) * ((0,0,p2)))),((((0,0,p1)) * ((0,0,p2))) - (((0,0,p1)) * ((0,0,p2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * p2 is V11() real V116() Element of REAL
p1 * 0 is V11() real V116() Element of REAL
(0 * p2) - (p1 * 0) is V11() real V116() Element of REAL
(p1 * 0) - (0 * p2) is V11() real V116() Element of REAL
0 * 0 is V11() real V116() Element of REAL
(0 * 0) - (0 * 0) is V11() real V116() Element of REAL
(((0 * p2) - (p1 * 0)),((p1 * 0) - (0 * p2)),((0 * 0) - (0 * 0))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 - p1 is V11() real V116() Element of REAL
0 * (p2 - p1) is V11() real V116() Element of REAL
p1 - p2 is V11() real V116() Element of REAL
0 * (p1 - p2) is V11() real V116() Element of REAL
0 * (0 * 0) is V11() real V116() Element of REAL
((0 * (p2 - p1)),(0 * (p1 - p2)),(0 * (0 * 0))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 - 0 is V11() real V116() Element of REAL
((p2 - p1),(p1 - p2),(0 - 0)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * ((p2 - p1),(p1 - p2),(0 - 0)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
0 * ((p2 - p1),(p1 - p2),(0 - 0)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 + p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) is V13() V16(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3))) V17( the carrier of (TOP-REAL 3)) Function-like V27(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) Element of K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)))
K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)) is set
K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) is set
K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3))) is set
the U5 of (TOP-REAL 3) . (p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 + p3 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1,(p2 + p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p2 + p3)) is V11() real V116() Element of REAL
(p2 + p3) . 3 is V11() real V116() Element of REAL
(p1) * ((p2 + p3)) is V11() real V116() Element of REAL
((p2 + p3)) is V11() real V116() Element of REAL
(p2 + p3) . 2 is V11() real V116() Element of REAL
(p1) * ((p2 + p3)) is V11() real V116() Element of REAL
((p1) * ((p2 + p3))) - ((p1) * ((p2 + p3))) is V11() real V116() Element of REAL
((p2 + p3)) is V11() real V116() Element of REAL
(p2 + p3) . 1 is V11() real V116() Element of REAL
(p1) * ((p2 + p3)) is V11() real V116() Element of REAL
(p1) * ((p2 + p3)) is V11() real V116() Element of REAL
((p1) * ((p2 + p3))) - ((p1) * ((p2 + p3))) is V11() real V116() Element of REAL
(p1) * ((p2 + p3)) is V11() real V116() Element of REAL
(p1) * ((p2 + p3)) is V11() real V116() Element of REAL
((p1) * ((p2 + p3))) - ((p1) * ((p2 + p3))) is V11() real V116() Element of REAL
((((p1) * ((p2 + p3))) - ((p1) * ((p2 + p3)))),(((p1) * ((p2 + p3))) - ((p1) * ((p2 + p3)))),(((p1) * ((p2 + p3))) - ((p1) * ((p2 + p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p3)) - ((p1) * (p3))),(((p1) * (p3)) - ((p1) * (p3))),(((p1) * (p3)) - ((p1) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2) + (p1,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((p1,p2),(p1,p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2) + (p1,p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(((p1) * (p2)) - ((p1) * (p2))) + (((p1) * (p3)) - ((p1) * (p3))) is V11() real V116() Element of REAL
(((p1) * (p2)) - ((p1) * (p2))) + (((p1) * (p3)) - ((p1) * (p3))) is V11() real V116() Element of REAL
(((p1) * (p2)) - ((p1) * (p2))) + (((p1) * (p3)) - ((p1) * (p3))) is V11() real V116() Element of REAL
(((((p1) * (p2)) - ((p1) * (p2))) + (((p1) * (p3)) - ((p1) * (p3)))),((((p1) * (p2)) - ((p1) * (p2))) + (((p1) * (p3)) - ((p1) * (p3)))),((((p1) * (p2)) - ((p1) * (p2))) + (((p1) * (p3)) - ((p1) * (p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3))) - ((p1) * (p3)) is V11() real V116() Element of REAL
(((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3))) - ((p1) * (p3)) is V11() real V116() Element of REAL
(((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3))) - ((p1) * (p3)) is V11() real V116() Element of REAL
((((((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3))) - ((p1) * (p3))),(((((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3))) - ((p1) * (p3))),(((((p1) * (p2)) - ((p1) * (p2))) + ((p1) * (p3))) - ((p1) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) + (p3) is V11() real V116() Element of REAL
(p2) + (p3) is V11() real V116() Element of REAL
(p2) + (p3) is V11() real V116() Element of REAL
(((p2) + (p3)),((p2) + (p3)),((p2) + (p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 + p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) is V13() V16(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3))) V17( the carrier of (TOP-REAL 3)) Function-like V27(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) Element of K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)))
K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)) is set
K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) is set
K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3))) is set
the U5 of (TOP-REAL 3) . (p1,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 + p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1 + p2),p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 2 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
((p1 + p2)) * (p3) is V11() real V116() Element of REAL
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 3 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
((p1 + p2)) * (p3) is V11() real V116() Element of REAL
(((p1 + p2)) * (p3)) - (((p1 + p2)) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
((p1 + p2)) * (p3) is V11() real V116() Element of REAL
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 1 is V11() real V116() Element of REAL
((p1 + p2)) * (p3) is V11() real V116() Element of REAL
(((p1 + p2)) * (p3)) - (((p1 + p2)) * (p3)) is V11() real V116() Element of REAL
((p1 + p2)) * (p3) is V11() real V116() Element of REAL
((p1 + p2)) * (p3) is V11() real V116() Element of REAL
(((p1 + p2)) * (p3)) - (((p1 + p2)) * (p3)) is V11() real V116() Element of REAL
(((((p1 + p2)) * (p3)) - (((p1 + p2)) * (p3))),((((p1 + p2)) * (p3)) - (((p1 + p2)) * (p3))),((((p1 + p2)) * (p3)) - (((p1 + p2)) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p3)) - ((p1) * (p3))),(((p1) * (p3)) - ((p1) * (p3))),(((p1) * (p3)) - ((p1) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p3) + (p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((p1,p3),(p2,p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p3) + (p2,p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p3,(p1 + p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3) * ((p1 + p2)) is V11() real V116() Element of REAL
(p3) * ((p1 + p2)) is V11() real V116() Element of REAL
((p3) * ((p1 + p2))) - ((p3) * ((p1 + p2))) is V11() real V116() Element of REAL
(p3) * ((p1 + p2)) is V11() real V116() Element of REAL
(p3) * ((p1 + p2)) is V11() real V116() Element of REAL
((p3) * ((p1 + p2))) - ((p3) * ((p1 + p2))) is V11() real V116() Element of REAL
(p3) * ((p1 + p2)) is V11() real V116() Element of REAL
(p3) * ((p1 + p2)) is V11() real V116() Element of REAL
((p3) * ((p1 + p2))) - ((p3) * ((p1 + p2))) is V11() real V116() Element of REAL
((((p3) * ((p1 + p2))) - ((p3) * ((p1 + p2)))),(((p3) * ((p1 + p2))) - ((p3) * ((p1 + p2)))),(((p3) * ((p1 + p2))) - ((p3) * ((p1 + p2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p3,(p1 + p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p3,(p1 + p2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p3,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3) * (p1) is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
((p3) * (p1)) - ((p3) * (p1)) is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
((p3) * (p1)) - ((p3) * (p1)) is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
((p3) * (p1)) - ((p3) * (p1)) is V11() real V116() Element of REAL
((((p3) * (p1)) - ((p3) * (p1))),(((p3) * (p1)) - ((p3) * (p1))),(((p3) * (p1)) - ((p3) * (p1)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3) * (p2) is V11() real V116() Element of REAL
(p3) * (p2) is V11() real V116() Element of REAL
((p3) * (p2)) - ((p3) * (p2)) is V11() real V116() Element of REAL
(p3) * (p2) is V11() real V116() Element of REAL
(p3) * (p2) is V11() real V116() Element of REAL
((p3) * (p2)) - ((p3) * (p2)) is V11() real V116() Element of REAL
(p3) * (p2) is V11() real V116() Element of REAL
(p3) * (p2) is V11() real V116() Element of REAL
((p3) * (p2)) - ((p3) * (p2)) is V11() real V116() Element of REAL
((((p3) * (p2)) - ((p3) * (p2))),(((p3) * (p2)) - ((p3) * (p2))),(((p3) * (p2)) - ((p3) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3,p1) + (p3,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((p3,p1),(p3,p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3,p1) + (p3,p2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
- ((p3,p1) + (p3,p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- ((p3,p1) + (p3,p2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p3,p1) - (p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p2,p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K237((TOP-REAL 3),(p3,p1),(- (p2,p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((p3,p1),(- (p2,p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3,p1) + (- (p2,p3)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p3,p1) - (p2,p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
- ((p3,p1) - (p2,p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- ((p3,p1) - (p2,p3)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
- (p3,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (p3,p1) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(- (p3,p1)) + (p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((- (p3,p1)),(p2,p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(- (p3,p1)) + (p2,p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p1) * (p1) is V11() real V116() Element of REAL
(p1) * (p1) is V11() real V116() Element of REAL
((p1) * (p1)) - ((p1) * (p1)) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p1) is V11() real V116() Element of REAL
(p1) * (p1) is V11() real V116() Element of REAL
((p1) * (p1)) - ((p1) * (p1)) is V11() real V116() Element of REAL
(p1) * (p1) is V11() real V116() Element of REAL
(p1) * (p1) is V11() real V116() Element of REAL
((p1) * (p1)) - ((p1) * (p1)) is V11() real V116() Element of REAL
((((p1) * (p1)) - ((p1) * (p1))),(((p1) * (p1)) - ((p1) * (p1))),(((p1) * (p1)) - ((p1) * (p1)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 + p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) is V13() V16(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3))) V17( the carrier of (TOP-REAL 3)) Function-like V27(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) Element of K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)))
K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)) is set
K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) is set
K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3))) is set
the U5 of (TOP-REAL 3) . (p1,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p1 + p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) - ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p3)) - ((p1) * (p3))),(((p1) * (p3)) - ((p1) * (p3))),(((p1) * (p3)) - ((p1) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
x2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p3 + x2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . (p3,x2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p3 + x2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1 + p2),(p3 + x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 2 is V11() real V116() Element of REAL
((p3 + x2)) is V11() real V116() Element of REAL
(p3 + x2) . 3 is V11() real V116() Element of REAL
((p1 + p2)) * ((p3 + x2)) is V11() real V116() Element of REAL
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 3 is V11() real V116() Element of REAL
((p3 + x2)) is V11() real V116() Element of REAL
(p3 + x2) . 2 is V11() real V116() Element of REAL
((p1 + p2)) * ((p3 + x2)) is V11() real V116() Element of REAL
(((p1 + p2)) * ((p3 + x2))) - (((p1 + p2)) * ((p3 + x2))) is V11() real V116() Element of REAL
((p3 + x2)) is V11() real V116() Element of REAL
(p3 + x2) . 1 is V11() real V116() Element of REAL
((p1 + p2)) * ((p3 + x2)) is V11() real V116() Element of REAL
((p1 + p2)) is V11() real V116() Element of REAL
(p1 + p2) . 1 is V11() real V116() Element of REAL
((p1 + p2)) * ((p3 + x2)) is V11() real V116() Element of REAL
(((p1 + p2)) * ((p3 + x2))) - (((p1 + p2)) * ((p3 + x2))) is V11() real V116() Element of REAL
((p1 + p2)) * ((p3 + x2)) is V11() real V116() Element of REAL
((p1 + p2)) * ((p3 + x2)) is V11() real V116() Element of REAL
(((p1 + p2)) * ((p3 + x2))) - (((p1 + p2)) * ((p3 + x2))) is V11() real V116() Element of REAL
(((((p1 + p2)) * ((p3 + x2))) - (((p1 + p2)) * ((p3 + x2)))),((((p1 + p2)) * ((p3 + x2))) - (((p1 + p2)) * ((p3 + x2)))),((((p1 + p2)) * ((p3 + x2))) - (((p1 + p2)) * ((p3 + x2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,x2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(x2) is V11() real V116() Element of REAL
x2 . 3 is V11() real V116() Element of REAL
(p1) * (x2) is V11() real V116() Element of REAL
(x2) is V11() real V116() Element of REAL
x2 . 2 is V11() real V116() Element of REAL
(p1) * (x2) is V11() real V116() Element of REAL
((p1) * (x2)) - ((p1) * (x2)) is V11() real V116() Element of REAL
(x2) is V11() real V116() Element of REAL
x2 . 1 is V11() real V116() Element of REAL
(p1) * (x2) is V11() real V116() Element of REAL
(p1) * (x2) is V11() real V116() Element of REAL
((p1) * (x2)) - ((p1) * (x2)) is V11() real V116() Element of REAL
(p1) * (x2) is V11() real V116() Element of REAL
(p1) * (x2) is V11() real V116() Element of REAL
((p1) * (x2)) - ((p1) * (x2)) is V11() real V116() Element of REAL
((((p1) * (x2)) - ((p1) * (x2))),(((p1) * (x2)) - ((p1) * (x2))),(((p1) * (x2)) - ((p1) * (x2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p3) + (p1,x2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((p1,p3),(p1,x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p3) + (p1,x2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1,p3) + (p1,x2)) + (p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . (((p1,p3) + (p1,x2)),(p2,p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p3) + (p1,x2)) + (p2,p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p2,x2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) * (x2) is V11() real V116() Element of REAL
(p2) * (x2) is V11() real V116() Element of REAL
((p2) * (x2)) - ((p2) * (x2)) is V11() real V116() Element of REAL
(p2) * (x2) is V11() real V116() Element of REAL
(p2) * (x2) is V11() real V116() Element of REAL
((p2) * (x2)) - ((p2) * (x2)) is V11() real V116() Element of REAL
(p2) * (x2) is V11() real V116() Element of REAL
(p2) * (x2) is V11() real V116() Element of REAL
((p2) * (x2)) - ((p2) * (x2)) is V11() real V116() Element of REAL
((((p2) * (x2)) - ((p2) * (x2))),(((p2) * (x2)) - ((p2) * (x2))),(((p2) * (x2)) - ((p2) * (x2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1,p3) + (p1,x2)) + (p2,p3)) + (p2,x2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((((p1,p3) + (p1,x2)) + (p2,p3)),(p2,x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1,p3) + (p1,x2)) + (p2,p3)) + (p2,x2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1,(p3 + x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) * ((p3 + x2)) is V11() real V116() Element of REAL
(p1) * ((p3 + x2)) is V11() real V116() Element of REAL
((p1) * ((p3 + x2))) - ((p1) * ((p3 + x2))) is V11() real V116() Element of REAL
(p1) * ((p3 + x2)) is V11() real V116() Element of REAL
(p1) * ((p3 + x2)) is V11() real V116() Element of REAL
((p1) * ((p3 + x2))) - ((p1) * ((p3 + x2))) is V11() real V116() Element of REAL
(p1) * ((p3 + x2)) is V11() real V116() Element of REAL
(p1) * ((p3 + x2)) is V11() real V116() Element of REAL
((p1) * ((p3 + x2))) - ((p1) * ((p3 + x2))) is V11() real V116() Element of REAL
((((p1) * ((p3 + x2))) - ((p1) * ((p3 + x2)))),(((p1) * ((p3 + x2))) - ((p1) * ((p3 + x2)))),(((p1) * ((p3 + x2))) - ((p1) * ((p3 + x2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,(p3 + x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) * ((p3 + x2)) is V11() real V116() Element of REAL
(p2) * ((p3 + x2)) is V11() real V116() Element of REAL
((p2) * ((p3 + x2))) - ((p2) * ((p3 + x2))) is V11() real V116() Element of REAL
(p2) * ((p3 + x2)) is V11() real V116() Element of REAL
(p2) * ((p3 + x2)) is V11() real V116() Element of REAL
((p2) * ((p3 + x2))) - ((p2) * ((p3 + x2))) is V11() real V116() Element of REAL
(p2) * ((p3 + x2)) is V11() real V116() Element of REAL
(p2) * ((p3 + x2)) is V11() real V116() Element of REAL
((p2) * ((p3 + x2))) - ((p2) * ((p3 + x2))) is V11() real V116() Element of REAL
((((p2) * ((p3 + x2))) - ((p2) * ((p3 + x2)))),(((p2) * ((p3 + x2))) - ((p2) * ((p3 + x2)))),(((p2) * ((p3 + x2))) - ((p2) * ((p3 + x2))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,(p3 + x2)) + (p2,(p3 + x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((p1,(p3 + x2)),(p2,(p3 + x2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,(p3 + x2)) + (p2,(p3 + x2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1,p3) + (p1,x2)) + (p2,(p3 + x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . (((p1,p3) + (p1,x2)),(p2,(p3 + x2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p3) + (p1,x2)) + (p2,(p3 + x2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p2,p3) + (p2,x2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((p2,p3),(p2,x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,p3) + (p2,x2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1,p3) + (p1,x2)) + ((p2,p3) + (p2,x2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . (((p1,p3) + (p1,x2)),((p2,p3) + (p2,x2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((p1,p3) + (p1,x2)) + ((p2,p3) + (p2,x2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
<*(p1),(p1),(p1)*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p3 is V11() real V116() Element of REAL
x2 is V11() real V116() Element of REAL
y1 is V11() real V116() Element of REAL
<*p3,x2,y1*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p2 is V13() Function-like FinSequence-like set
p2 . 1 is set
<*(p2 . 1),x2,y1*> is set
p2 . 2 is set
<*(p2 . 1),(p2 . 2),y1*> is set
p1 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
len p1 is natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() Element of NAT
p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
len p2 is natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() Element of NAT
mlt (p1,p2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 . 1 is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1 . 1) * (p2 . 1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1 . 2) * (p2 . 2) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1 . 3) * (p2 . 3) is V11() real V116() Element of REAL
<*((p1 . 1) * (p2 . 1)),((p1 . 2) * (p2 . 2)),((p1 . 3) * (p2 . 3))*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
<*(p2 . 1),(p2 . 2),(p2 . 3)*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
multreal .: (p1,p2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
<*(p1 . 1),(p1 . 2),(p1 . 3)*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
multreal .: (<*(p1 . 1),(p1 . 2),(p1 . 3)*>,<*(p2 . 1),(p2 . 2),(p2 . 3)*>) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
multreal . ((p1 . 1),(p2 . 1)) is V11() real V116() Element of REAL
multreal . ((p1 . 2),(p2 . 2)) is V11() real V116() Element of REAL
multreal . ((p1 . 3),(p2 . 3)) is V11() real V116() Element of REAL
<*(multreal . ((p1 . 1),(p2 . 1))),(multreal . ((p1 . 2),(p2 . 2))),(multreal . ((p1 . 3),(p2 . 3)))*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
<*((p1 . 1) * (p2 . 1)),(multreal . ((p1 . 2),(p2 . 2))),(multreal . ((p1 . 3),(p2 . 3)))*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
<*((p1 . 1) * (p2 . 1)),((p1 . 2) * (p2 . 2)),(multreal . ((p1 . 3),(p2 . 3)))*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,p2)| is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) + ((p1) * (p2)) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2)) is V11() real V116() Element of REAL
p3 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
len p3 is natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() Element of NAT
<*(p1),(p1),(p1)*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
len <*(p1),(p1),(p1)*> is natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() Element of NAT
x2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
len x2 is natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() Element of NAT
<*(p2),(p2),(p2)*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
len <*(p2),(p2),(p2)*> is natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() Element of NAT
mlt (p3,x2) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (mlt (p3,x2)) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
x2 . 1 is V11() real V116() Element of REAL
(p3 . 1) * (x2 . 1) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
x2 . 2 is V11() real V116() Element of REAL
(p3 . 2) * (x2 . 2) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
x2 . 3 is V11() real V116() Element of REAL
(p3 . 3) * (x2 . 3) is V11() real V116() Element of REAL
<*((p3 . 1) * (x2 . 1)),((p3 . 2) * (x2 . 2)),((p3 . 3) * (x2 . 3))*> is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum <*((p3 . 1) * (x2 . 1)),((p3 . 2) * (x2 . 2)),((p3 . 3) * (x2 . 3))*> is V11() real V116() Element of REAL
(p1) * (x2 . 3) is V11() real V116() Element of REAL
(((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (x2 . 3)) is V11() real V116() Element of REAL
p1 is V11() real V116() Element of REAL
p2 is V11() real V116() Element of REAL
p1 * p2 is V11() real V116() Element of REAL
p3 is V11() real V116() Element of REAL
x2 is V11() real V116() Element of REAL
(p3,x2,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
y1 is V11() real V116() Element of REAL
p3 * y1 is V11() real V116() Element of REAL
y2 is V11() real V116() Element of REAL
(y1,y2,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|((p3,x2,p1),(y1,y2,p2))| is V11() real V116() Element of REAL
x2 * y2 is V11() real V116() Element of REAL
(p3 * y1) + (x2 * y2) is V11() real V116() Element of REAL
((p3 * y1) + (x2 * y2)) + (p1 * p2) is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,(p2,p3))| is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p1,p2) is V11() real V116() set
(p1,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,(p1,p2))| is V11() real V116() Element of REAL
(p2,p1,p2) is V11() real V116() set
|(p2,(p1,p2))| is V11() real V116() Element of REAL
((p1,p2)) is V11() real V116() Element of REAL
(p1,p2) . 1 is V11() real V116() Element of REAL
(p2) * ((p1,p2)) is V11() real V116() Element of REAL
((p1,p2)) is V11() real V116() Element of REAL
(p1,p2) . 2 is V11() real V116() Element of REAL
(p2) * ((p1,p2)) is V11() real V116() Element of REAL
((p2) * ((p1,p2))) + ((p2) * ((p1,p2))) is V11() real V116() Element of REAL
((p1,p2)) is V11() real V116() Element of REAL
(p1,p2) . 3 is V11() real V116() Element of REAL
(p2) * ((p1,p2)) is V11() real V116() Element of REAL
(((p2) * ((p1,p2))) + ((p2) * ((p1,p2)))) + ((p2) * ((p1,p2))) is V11() real V116() Element of REAL
(p2) * (((p1) * (p2)) - ((p1) * (p2))) is V11() real V116() Element of REAL
((p2) * (((p1) * (p2)) - ((p1) * (p2)))) + ((p2) * ((p1,p2))) is V11() real V116() Element of REAL
(((p2) * (((p1) * (p2)) - ((p1) * (p2)))) + ((p2) * ((p1,p2)))) + ((p2) * ((p1,p2))) is V11() real V116() Element of REAL
(p2) * (((p1) * (p2)) - ((p1) * (p2))) is V11() real V116() Element of REAL
((p2) * (((p1) * (p2)) - ((p1) * (p2)))) + ((p2) * (((p1) * (p2)) - ((p1) * (p2)))) is V11() real V116() Element of REAL
(((p2) * (((p1) * (p2)) - ((p1) * (p2)))) + ((p2) * (((p1) * (p2)) - ((p1) * (p2))))) + ((p2) * ((p1,p2))) is V11() real V116() Element of REAL
(p2) * ((p1) * (p2)) is V11() real V116() Element of REAL
(p2) * ((p1) * (p2)) is V11() real V116() Element of REAL
((p2) * ((p1) * (p2))) - ((p2) * ((p1) * (p2))) is V11() real V116() Element of REAL
(((p2) * ((p1) * (p2))) - ((p2) * ((p1) * (p2)))) + ((p2) * (((p1) * (p2)) - ((p1) * (p2)))) is V11() real V116() Element of REAL
(p2) * (((p1) * (p2)) - ((p1) * (p2))) is V11() real V116() Element of REAL
((((p2) * ((p1) * (p2))) - ((p2) * ((p1) * (p2)))) + ((p2) * (((p1) * (p2)) - ((p1) * (p2))))) + ((p2) * (((p1) * (p2)) - ((p1) * (p2)))) is V11() real V116() Element of REAL
(p2) * ((p1) * (p2)) is V11() real V116() Element of REAL
0 - ((p2) * ((p1) * (p2))) is V11() real V116() Element of REAL
(0 - ((p2) * ((p1) * (p2)))) + ((p2) * ((p1) * (p2))) is V11() real V116() Element of REAL
(p1) * ((p1,p2)) is V11() real V116() Element of REAL
(p1) * ((p1,p2)) is V11() real V116() Element of REAL
((p1) * ((p1,p2))) + ((p1) * ((p1,p2))) is V11() real V116() Element of REAL
(p1) * ((p1,p2)) is V11() real V116() Element of REAL
(((p1) * ((p1,p2))) + ((p1) * ((p1,p2)))) + ((p1) * ((p1,p2))) is V11() real V116() Element of REAL
(p1) * (((p1) * (p2)) - ((p1) * (p2))) is V11() real V116() Element of REAL
((p1) * (((p1) * (p2)) - ((p1) * (p2)))) + ((p1) * ((p1,p2))) is V11() real V116() Element of REAL
(((p1) * (((p1) * (p2)) - ((p1) * (p2)))) + ((p1) * ((p1,p2)))) + ((p1) * ((p1,p2))) is V11() real V116() Element of REAL
(p1) * (((p1) * (p2)) - ((p1) * (p2))) is V11() real V116() Element of REAL
((p1) * (((p1) * (p2)) - ((p1) * (p2)))) + ((p1) * (((p1) * (p2)) - ((p1) * (p2)))) is V11() real V116() Element of REAL
(((p1) * (((p1) * (p2)) - ((p1) * (p2)))) + ((p1) * (((p1) * (p2)) - ((p1) * (p2))))) + ((p1) * ((p1,p2))) is V11() real V116() Element of REAL
(p1) * ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * ((p1) * (p2)) is V11() real V116() Element of REAL
((p1) * ((p1) * (p2))) - ((p1) * ((p1) * (p2))) is V11() real V116() Element of REAL
(((p1) * ((p1) * (p2))) - ((p1) * ((p1) * (p2)))) + ((p1) * (((p1) * (p2)) - ((p1) * (p2)))) is V11() real V116() Element of REAL
(p1) * (((p1) * (p2)) - ((p1) * (p2))) is V11() real V116() Element of REAL
((((p1) * ((p1) * (p2))) - ((p1) * ((p1) * (p2)))) + ((p1) * (((p1) * (p2)) - ((p1) * (p2))))) + ((p1) * (((p1) * (p2)) - ((p1) * (p2)))) is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,p2)| is V11() real V116() Element of REAL
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,(p2,p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
((p2,p3)) is V11() real V116() Element of REAL
(p2,p3) . 3 is V11() real V116() Element of REAL
(p1) * ((p2,p3)) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
((p2,p3)) is V11() real V116() Element of REAL
(p2,p3) . 2 is V11() real V116() Element of REAL
(p1) * ((p2,p3)) is V11() real V116() Element of REAL
((p1) * ((p2,p3))) - ((p1) * ((p2,p3))) is V11() real V116() Element of REAL
((p2,p3)) is V11() real V116() Element of REAL
(p2,p3) . 1 is V11() real V116() Element of REAL
(p1) * ((p2,p3)) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * ((p2,p3)) is V11() real V116() Element of REAL
((p1) * ((p2,p3))) - ((p1) * ((p2,p3))) is V11() real V116() Element of REAL
(p1) * ((p2,p3)) is V11() real V116() Element of REAL
(p1) * ((p2,p3)) is V11() real V116() Element of REAL
((p1) * ((p2,p3))) - ((p1) * ((p2,p3))) is V11() real V116() Element of REAL
((((p1) * ((p2,p3))) - ((p1) * ((p2,p3)))),(((p1) * ((p2,p3))) - ((p1) * ((p2,p3)))),(((p1) * ((p2,p3))) - ((p1) * ((p2,p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,p3)| is V11() real V116() Element of REAL
|(p1,p3)| * p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,p3)| * p2 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
|(p1,p2)| * p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,p2)| * p3 is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(|(p1,p3)| * p2) - (|(p1,p2)| * p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (|(p1,p2)| * p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (|(p1,p2)| * p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K237((TOP-REAL 3),(|(p1,p3)| * p2),(- (|(p1,p2)| * p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) is V13() V16(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3))) V17( the carrier of (TOP-REAL 3)) Function-like V27(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) Element of K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)))
K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)) is set
K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3)) is set
K6(K7(K7( the carrier of (TOP-REAL 3), the carrier of (TOP-REAL 3)), the carrier of (TOP-REAL 3))) is set
the U5 of (TOP-REAL 3) . ((|(p1,p3)| * p2),(- (|(p1,p2)| * p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(|(p1,p3)| * p2) + (- (|(p1,p2)| * p3)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(|(p1,p3)| * p2) - (|(p1,p2)| * p3) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
((p1) * (((p2) * (p3)) - ((p2) * (p3)))) - ((p1) * (((p2) * (p3)) - ((p2) * (p3)))) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
((p1) * (p3)) + ((p1) * (p3)) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) + ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3) is V11() real V116() Element of REAL
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)) - (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
((p1) * (((p2) * (p3)) - ((p2) * (p3)))) - ((p1) * (((p2) * (p3)) - ((p2) * (p3)))) is V11() real V116() Element of REAL
((p1) * (p3)) + ((p1) * (p3)) is V11() real V116() Element of REAL
(((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) + ((p1) * (p2)) is V11() real V116() Element of REAL
(((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3) is V11() real V116() Element of REAL
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)) - (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
((p1) * (((p2) * (p3)) - ((p2) * (p3)))) - ((p1) * (((p2) * (p3)) - ((p2) * (p3)))) is V11() real V116() Element of REAL
((p1) * (p3)) + ((p1) * (p3)) is V11() real V116() Element of REAL
(((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3)) is V11() real V116() Element of REAL
((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) + ((p1) * (p2)) is V11() real V116() Element of REAL
(((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3) is V11() real V116() Element of REAL
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)) - (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)) is V11() real V116() Element of REAL
((p1),(p1),(p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1),(p1),(p1)),((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((p1),(p1),(p1))) is V11() real V116() Element of REAL
((p1),(p1),(p1)) . 2 is V11() real V116() Element of REAL
(((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) . 3 is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) is V11() real V116() Element of REAL
((p1),(p1),(p1)) . 3 is V11() real V116() Element of REAL
(((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) . 2 is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) - ((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) is V11() real V116() Element of REAL
(((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) . 1 is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) is V11() real V116() Element of REAL
((p1),(p1),(p1)) . 1 is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) - ((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
(((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))) is V11() real V116() Element of REAL
((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) - ((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) is V11() real V116() Element of REAL
((((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) - ((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))))),(((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) - ((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))))))),(((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))) - ((((p1),(p1),(p1))) * (((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((p1) * (((p2) * (p3)) - ((p2) * (p3)))) - ((p1) * (((p2) * (p3)) - ((p2) * (p3))))),(((p1) * (((p2) * (p3)) - ((p2) * (p3)))) - ((p1) * (((p2) * (p3)) - ((p2) * (p3))))),(((p1) * (((p2) * (p3)) - ((p2) * (p3)))) - ((p1) * (((p2) * (p3)) - ((p2) * (p3)))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2) is V11() real V116() Element of REAL
((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2) is V11() real V116() Element of REAL
((((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3) is V11() real V116() Element of REAL
((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3) is V11() real V116() Element of REAL
((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2))) - ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K237((TOP-REAL 3),((((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2))),(- ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . (((((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2))),(- ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2))) + (- ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2)),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * (p2))) - ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p2),(p2),(p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))) - ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
K237((TOP-REAL 3),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))),(- ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))),(- ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))) + (- ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))) - ((((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3)),(((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * (p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p3),(p3),(p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))) - (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K237((TOP-REAL 3),(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))),(- (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))),(- (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))) + (- (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3)))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(((((p1) * (p3)) + ((p1) * (p3))) + ((p1) * (p3))) * ((p2),(p2),(p2))) - (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
|(p1,p3)| * ((p2),(p2),(p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,p3)| * ((p2),(p2),(p2)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(|(p1,p3)| * ((p2),(p2),(p2))) - (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
K237((TOP-REAL 3),(|(p1,p3)| * ((p2),(p2),(p2))),(- (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((|(p1,p3)| * ((p2),(p2),(p2))),(- (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(|(p1,p3)| * ((p2),(p2),(p2))) + (- (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3)))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(|(p1,p3)| * ((p2),(p2),(p2))) - (((((p1) * (p2)) + ((p1) * (p2))) + ((p1) * (p2))) * ((p3),(p3),(p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
|(p1,p2)| * ((p3),(p3),(p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,p2)| * ((p3),(p3),(p3)) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(|(p1,p3)| * ((p2),(p2),(p2))) - (|(p1,p2)| * ((p3),(p3),(p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (|(p1,p2)| * ((p3),(p3),(p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
- (|(p1,p2)| * ((p3),(p3),(p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K237((TOP-REAL 3),(|(p1,p3)| * ((p2),(p2),(p2))),(- (|(p1,p2)| * ((p3),(p3),(p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((|(p1,p3)| * ((p2),(p2),(p2))),(- (|(p1,p2)| * ((p3),(p3),(p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(|(p1,p3)| * ((p2),(p2),(p2))) + (- (|(p1,p2)| * ((p3),(p3),(p3)))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(|(p1,p3)| * ((p2),(p2),(p2))) - (|(p1,p2)| * ((p3),(p3),(p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(|(p1,p3)| * p2) - (|(p1,p2)| * ((p3),(p3),(p3))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
K237((TOP-REAL 3),(|(p1,p3)| * p2),(- (|(p1,p2)| * ((p3),(p3),(p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
the U5 of (TOP-REAL 3) . ((|(p1,p3)| * p2),(- (|(p1,p2)| * ((p3),(p3),(p3))))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(|(p1,p3)| * p2) + (- (|(p1,p2)| * ((p3),(p3),(p3)))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(|(p1,p3)| * p2) - (|(p1,p2)| * ((p3),(p3),(p3))) is V13() V16( NAT ) V17( REAL ) Function-like FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2,p3) is V11() real V116() set
(p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,(p2,p3))| is V11() real V116() Element of REAL
(p2,p3,p1) is V11() real V116() set
(p3,p1) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
((p3) * (p1)) - ((p3) * (p1)) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
((p3) * (p1)) - ((p3) * (p1)) is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
(p3) * (p1) is V11() real V116() Element of REAL
((p3) * (p1)) - ((p3) * (p1)) is V11() real V116() Element of REAL
((((p3) * (p1)) - ((p3) * (p1))),(((p3) * (p1)) - ((p3) * (p1))),(((p3) * (p1)) - ((p3) * (p1)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p2,(p3,p1))| is V11() real V116() Element of REAL
((p1),(p1),(p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(((p1),(p1),(p1)),((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))| is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
((p1) * (((p2) * (p3)) - ((p2) * (p3)))) + ((p1) * (((p2) * (p3)) - ((p2) * (p3)))) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
(((p1) * (((p2) * (p3)) - ((p2) * (p3)))) + ((p1) * (((p2) * (p3)) - ((p2) * (p3))))) + ((p1) * (((p2) * (p3)) - ((p2) * (p3)))) is V11() real V116() Element of REAL
(p2) * (((p3) * (p1)) - ((p3) * (p1))) is V11() real V116() Element of REAL
(p2) * (((p3) * (p1)) - ((p3) * (p1))) is V11() real V116() Element of REAL
((p2) * (((p3) * (p1)) - ((p3) * (p1)))) + ((p2) * (((p3) * (p1)) - ((p3) * (p1)))) is V11() real V116() Element of REAL
(p2) * (((p3) * (p1)) - ((p3) * (p1))) is V11() real V116() Element of REAL
(((p2) * (((p3) * (p1)) - ((p3) * (p1)))) + ((p2) * (((p3) * (p1)) - ((p3) * (p1))))) + ((p2) * (((p3) * (p1)) - ((p3) * (p1)))) is V11() real V116() Element of REAL
((p2),(p2),(p2)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(((p2),(p2),(p2)),((((p3) * (p1)) - ((p3) * (p1))),(((p3) * (p1)) - ((p3) * (p1))),(((p3) * (p1)) - ((p3) * (p1)))))| is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2,p3) is V11() real V116() set
(p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,(p2,p3))| is V11() real V116() Element of REAL
(p3,p1,p2) is V11() real V116() set
(p1,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p3,(p1,p2))| is V11() real V116() Element of REAL
p1 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p2 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1) is V11() real V116() Element of REAL
p1 . 2 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 3 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 3 is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 2 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p2) is V11() real V116() Element of REAL
p2 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) is V11() real V116() Element of REAL
p1 . 1 is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
(p1) * (p2) is V11() real V116() Element of REAL
((p1) * (p2)) - ((p1) * (p2)) is V11() real V116() Element of REAL
((((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2))),(((p1) * (p2)) - ((p1) * (p2)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
p3 is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p1,p2,p3) is V11() real V116() set
(p2,p3) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
(p3) is V11() real V116() Element of REAL
p3 . 3 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 2 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p3) is V11() real V116() Element of REAL
p3 . 1 is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
(p2) * (p3) is V11() real V116() Element of REAL
((p2) * (p3)) - ((p2) * (p3)) is V11() real V116() Element of REAL
((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(p1,(p2,p3))| is V11() real V116() Element of REAL
|((p1,p2),p3)| is V11() real V116() Element of REAL
((p1),(p1),(p1)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|(((p1),(p1),(p1)),((((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3))),(((p2) * (p3)) - ((p2) * (p3)))))| is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
((p1) * (((p2) * (p3)) - ((p2) * (p3)))) + ((p1) * (((p2) * (p3)) - ((p2) * (p3)))) is V11() real V116() Element of REAL
(p1) * (((p2) * (p3)) - ((p2) * (p3))) is V11() real V116() Element of REAL
(((p1) * (((p2) * (p3)) - ((p2) * (p3)))) + ((p1) * (((p2) * (p3)) - ((p2) * (p3))))) + ((p1) * (((p2) * (p3)) - ((p2) * (p3)))) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p2) * ((p1) * (p3)) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p2) * ((p1) * (p3)) is V11() real V116() Element of REAL
((p2) * ((p1) * (p3))) - ((p2) * ((p1) * (p3))) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p2) * ((p1) * (p3)) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p2) * ((p1) * (p3)) is V11() real V116() Element of REAL
((p2) * ((p1) * (p3))) - ((p2) * ((p1) * (p3))) is V11() real V116() Element of REAL
(((p2) * ((p1) * (p3))) - ((p2) * ((p1) * (p3)))) + (((p2) * ((p1) * (p3))) - ((p2) * ((p1) * (p3)))) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p2) * ((p1) * (p3)) is V11() real V116() Element of REAL
(p1) * (p3) is V11() real V116() Element of REAL
(p2) * ((p1) * (p3)) is V11() real V116() Element of REAL
((p2) * ((p1) * (p3))) - ((p2) * ((p1) * (p3))) is V11() real V116() Element of REAL
((((p2) * ((p1) * (p3))) - ((p2) * ((p1) * (p3)))) + (((p2) * ((p1) * (p3))) - ((p2) * ((p1) * (p3))))) + (((p2) * ((p1) * (p3))) - ((p2) * ((p1) * (p3)))) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
((p2) * (p1)) - ((p2) * (p1)) is V11() real V116() Element of REAL
(((p2) * (p1)) - ((p2) * (p1))) * (p3) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
((p2) * (p1)) - ((p2) * (p1)) is V11() real V116() Element of REAL
(((p2) * (p1)) - ((p2) * (p1))) * (p3) is V11() real V116() Element of REAL
((((p2) * (p1)) - ((p2) * (p1))) * (p3)) + ((((p2) * (p1)) - ((p2) * (p1))) * (p3)) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
(p2) * (p1) is V11() real V116() Element of REAL
((p2) * (p1)) - ((p2) * (p1)) is V11() real V116() Element of REAL
(((p2) * (p1)) - ((p2) * (p1))) * (p3) is V11() real V116() Element of REAL
(((((p2) * (p1)) - ((p2) * (p1))) * (p3)) + ((((p2) * (p1)) - ((p2) * (p1))) * (p3))) + ((((p2) * (p1)) - ((p2) * (p1))) * (p3)) is V11() real V116() Element of REAL
((p3),(p3),(p3)) is V13() Function-like V41(3) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 3)
|((p1,p2),((p3),(p3),(p3)))| is V11() real V116() Element of REAL