REAL is non empty V38() V129() V130() V131() V135() set
NAT is V129() V130() V131() V132() V133() V134() V135() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V38() V129() V135() set
RAT is non empty V38() V129() V130() V131() V132() V135() set
INT is non empty V38() 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 RAT -valued complex-yielding V120() V121() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued complex-yielding V120() V121() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued complex-yielding V120() V121() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued complex-yielding V120() V121() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7(K7(NAT,NAT),NAT)) is set
K7(NAT,REAL) is complex-yielding V120() V121() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is complex-yielding set
K6(K7(NAT,COMPLEX)) is set
omega is V129() V130() V131() V132() V133() V134() V135() set
K6(omega) is set
K6(NAT) is set
K391() is non empty V78() L8()
the carrier of K391() is non empty set
K396() is non empty V78() V100() V101() V102() V104() V151() V152() V153() V154() V155() V156() L8()
K397() is non empty V78() V102() V104() V154() V155() V156() M15(K396())
K398() is non empty V78() V100() V102() V104() V154() V155() V156() V157() M18(K396(),K397())
K400() is non empty V78() V100() V102() V104() L8()
K401() is non empty V78() V100() V102() V104() V157() M15(K400())
K486() is V204() TopStruct
the carrier of K486() is V129() V130() V131() set
1 is non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() Element of NAT
K7(1,1) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued 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 non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() Element of NAT
K7(2,2) is RAT -valued INT -valued 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
K514() is V190() V204() L14()
R^1 is non empty strict TopSpace-like V204() TopStruct
TOP-REAL 2 is non empty V76() V141() V142() TopSpace-like V206() V207() V208() V209() V210() V211() V212() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K6( the carrier of (TOP-REAL 2)) is set
{} is empty V129() V130() V131() V132() V133() V134() V135() set
the empty V129() V130() V131() V132() V133() V134() V135() set is empty V129() V130() V131() V132() V133() V134() V135() set
0 is empty natural complex V12() ext-real non positive non negative V33() V34() V129() V130() V131() V132() V133() V134() V135() Element of NAT
Re 0 is complex V12() ext-real Element of REAL
Im 0 is complex V12() ext-real Element of REAL
<i> is complex Element of COMPLEX
- 1 is non empty complex V12() ext-real non positive negative Element of REAL
0. (TOP-REAL 2) is Relation-like V21() V45(2) FinSequence-like zero complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|[0,0]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
PI is complex V12() ext-real Element of REAL
].0,PI.[ is V129() V130() V131() Element of K6(REAL)
2 * PI is complex V12() ext-real Element of REAL
PI / 2 is complex V12() ext-real Element of COMPLEX
3 is non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() Element of NAT
3 / 2 is non empty complex V12() ext-real positive non negative Element of COMPLEX
(3 / 2) * PI is complex V12() ext-real Element of REAL
4 is non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() Element of NAT
K150(1,4) is non empty complex V12() ext-real positive non negative V34() Element of RAT
the carrier of R^1 is non empty V129() V130() V131() set
p1 is complex set
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
p1 is complex set
(p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
((p1)) is complex Element of COMPLEX
(p1) `1 is complex V12() ext-real Element of REAL
(p1) . 1 is complex V12() ext-real Element of REAL
(p1) `2 is complex V12() ext-real Element of REAL
(p1) . 2 is complex V12() ext-real Element of REAL
((p1) `2) * <i> is complex set
((p1) `1) + (((p1) `2) * <i>) is complex set
|[(Re p1),(Im p1)]| `1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| . 1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| `2 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| . 2 is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
((p1)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (p1) is complex V12() ext-real Element of REAL
Im (p1) is complex V12() ext-real Element of REAL
|[(Re (p1)),(Im (p1))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re ((p1 `1) + ((p1 `2) * <i>)) is complex V12() ext-real Element of REAL
Im ((p1 `1) + ((p1 `2) * <i>)) is complex V12() ext-real Element of REAL
p1 is complex set
(p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 is complex set
(p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p2 is complex V12() ext-real Element of REAL
Im p2 is complex V12() ext-real Element of REAL
|[(Re p2),(Im p2)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
((p2)) is complex Element of COMPLEX
(p2) `1 is complex V12() ext-real Element of REAL
(p2) . 1 is complex V12() ext-real Element of REAL
(p2) `2 is complex V12() ext-real Element of REAL
(p2) . 2 is complex V12() ext-real Element of REAL
((p2) `2) * <i> is complex set
((p2) `1) + (((p2) `2) * <i>) is complex set
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p2) is complex Element of COMPLEX
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
((p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (p2) is complex V12() ext-real Element of REAL
Im (p2) is complex V12() ext-real Element of REAL
|[(Re (p2)),(Im (p2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 is complex V12() ext-real Element of REAL
p2 is complex V12() ext-real Element of REAL
p2 * <i> is complex set
p1 + (p2 * <i>) is complex set
((p1 + (p2 * <i>))) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (p1 + (p2 * <i>)) is complex V12() ext-real Element of REAL
Im (p1 + (p2 * <i>)) is complex V12() ext-real Element of REAL
|[(Re (p1 + (p2 * <i>))),(Im (p1 + (p2 * <i>)))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|[p1,p2]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 is complex set
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
p2 is complex set
p1 + p2 is complex set
Re (p1 + p2) is complex V12() ext-real Element of REAL
Im (p1 + p2) is complex V12() ext-real Element of REAL
|[(Re (p1 + p2)),(Im (p1 + p2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p2 is complex V12() ext-real Element of REAL
(Re p1) + (Re p2) is complex V12() ext-real Element of REAL
Im p2 is complex V12() ext-real Element of REAL
(Im p1) + (Im p2) is complex V12() ext-real Element of REAL
|[((Re p1) + (Re p2)),((Im p1) + (Im p2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|[(Re (p1 + p2)),(Im (p1 + p2))]| `2 is complex V12() ext-real Element of REAL
|[(Re (p1 + p2)),(Im (p1 + p2))]| . 2 is complex V12() ext-real Element of REAL
|[(Re (p1 + p2)),(Im (p1 + p2))]| `1 is complex V12() ext-real Element of REAL
|[(Re (p1 + p2)),(Im (p1 + p2))]| . 1 is complex V12() ext-real Element of REAL
p1 is complex set
(p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 is complex set
p1 + p2 is complex set
((p1 + p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (p1 + p2) is complex V12() ext-real Element of REAL
Im (p1 + p2) is complex V12() ext-real Element of REAL
|[(Re (p1 + p2)),(Im (p1 + p2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p2 is complex V12() ext-real Element of REAL
Im p2 is complex V12() ext-real Element of REAL
|[(Re p2),(Im p2)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) + (p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued V21() V30(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),(p1),(p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) + (p2) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(Re p1) + (Re p2) is complex V12() ext-real Element of REAL
(Im p1) + (Im p2) is complex V12() ext-real Element of REAL
|[((Re p1) + (Re p2)),((Im p1) + (Im p2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 + p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued V21() V30(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 + p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1 + p2) `1 is complex V12() ext-real Element of REAL
(p1 + p2) . 1 is complex V12() ext-real Element of REAL
(p1 + p2) `2 is complex V12() ext-real Element of REAL
(p1 + p2) . 2 is complex V12() ext-real Element of REAL
((p1 + p2) `2) * <i> is complex set
((p1 + p2) `1) + (((p1 + p2) `2) * <i>) is complex set
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
(p1 `1) + (p2 `1) is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p1 `2) + (p2 `2) is complex V12() ext-real Element of REAL
((p1 `2) + (p2 `2)) * <i> is complex set
((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>) is complex set
|[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Im (((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)) is complex V12() ext-real Element of REAL
Im (((p1 + p2) `1) + (((p1 + p2) `2) * <i>)) is complex V12() ext-real Element of REAL
Re (((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)) is complex V12() ext-real Element of REAL
Re (((p1 + p2) `1) + (((p1 + p2) `2) * <i>)) is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 + p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued V21() V30(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 + p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1 + p2)) is complex Element of COMPLEX
(p1 + p2) `1 is complex V12() ext-real Element of REAL
(p1 + p2) . 1 is complex V12() ext-real Element of REAL
(p1 + p2) `2 is complex V12() ext-real Element of REAL
(p1 + p2) . 2 is complex V12() ext-real Element of REAL
((p1 + p2) `2) * <i> is complex set
((p1 + p2) `1) + (((p1 + p2) `2) * <i>) is complex set
(p2) is complex Element of COMPLEX
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
(p1) + (p2) is complex Element of COMPLEX
(p1 `1) + (p2 `1) is complex V12() ext-real Element of REAL
(p1 `2) + (p2 `2) is complex V12() ext-real Element of REAL
((p1 `2) + (p2 `2)) * <i> is complex set
((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>) is complex set
p1 is complex set
- p1 is complex set
Re (- p1) is complex V12() ext-real Element of REAL
Im (- p1) is complex V12() ext-real Element of REAL
|[(Re (- p1)),(Im (- p1))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
- (Re p1) is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
- (Im p1) is complex V12() ext-real Element of REAL
|[(- (Re p1)),(- (Im p1))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|[(Re (- p1)),(Im (- p1))]| `2 is complex V12() ext-real Element of REAL
|[(Re (- p1)),(Im (- p1))]| . 2 is complex V12() ext-real Element of REAL
|[(Re (- p1)),(Im (- p1))]| `1 is complex V12() ext-real Element of REAL
|[(Re (- p1)),(Im (- p1))]| . 1 is complex V12() ext-real Element of REAL
p1 is complex set
- p1 is complex set
((- p1)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (- p1) is complex V12() ext-real Element of REAL
Im (- p1) is complex V12() ext-real Element of REAL
|[(Re (- p1)),(Im (- p1))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- (p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- (p1) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
- (Re p1) is complex V12() ext-real Element of REAL
- (Im p1) is complex V12() ext-real Element of REAL
|[(- (Re p1)),(- (Im p1))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(- p1) `1 is complex V12() ext-real Element of REAL
(- p1) . 1 is complex V12() ext-real Element of REAL
(- p1) `2 is complex V12() ext-real Element of REAL
(- p1) . 2 is complex V12() ext-real Element of REAL
((- p1) `2) * <i> is complex set
((- p1) `1) + (((- p1) `2) * <i>) is complex set
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
- (p1 `1) is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
- (p1 `2) is complex V12() ext-real Element of REAL
(- (p1 `2)) * <i> is complex set
(- (p1 `1)) + ((- (p1 `2)) * <i>) is complex set
|[(- (p1 `1)),(- (p1 `2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1 `2) * <i> is complex set
- ((p1 `2) * <i>) is complex set
(- (p1 `1)) + (- ((p1 `2) * <i>)) is complex set
Re ((- (p1 `1)) + (- ((p1 `2) * <i>))) is complex V12() ext-real Element of REAL
Im ((- (p1 `1)) + (- ((p1 `2) * <i>))) is complex V12() ext-real Element of REAL
Re (((- p1) `1) + (((- p1) `2) * <i>)) is complex V12() ext-real Element of REAL
Im (((- p1) `1) + (((- p1) `2) * <i>)) is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((- p1)) is complex Element of COMPLEX
(- p1) `1 is complex V12() ext-real Element of REAL
(- p1) . 1 is complex V12() ext-real Element of REAL
(- p1) `2 is complex V12() ext-real Element of REAL
(- p1) . 2 is complex V12() ext-real Element of REAL
((- p1) `2) * <i> is complex set
((- p1) `1) + (((- p1) `2) * <i>) is complex set
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
- (p1) is complex Element of COMPLEX
- (p1 `1) is complex V12() ext-real Element of REAL
- (p1 `2) is complex V12() ext-real Element of REAL
(- (p1 `2)) * <i> is complex set
(- (p1 `1)) + ((- (p1 `2)) * <i>) is complex set
p1 is complex set
(p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 is complex set
p1 - p2 is complex set
((p1 - p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (p1 - p2) is complex V12() ext-real Element of REAL
Im (p1 - p2) is complex V12() ext-real Element of REAL
|[(Re (p1 - p2)),(Im (p1 - p2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p2 is complex V12() ext-real Element of REAL
Im p2 is complex V12() ext-real Element of REAL
|[(Re p2),(Im p2)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) - (p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- (p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- (p2) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K259((TOP-REAL 2),(p1),(- (p2))) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued V21() V30(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),(p1),(- (p2))) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) + (- (p2)) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1) - (p2) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
- p2 is complex set
p1 + (- p2) is complex set
((p1 + (- p2))) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (p1 + (- p2)) is complex V12() ext-real Element of REAL
Im (p1 + (- p2)) is complex V12() ext-real Element of REAL
|[(Re (p1 + (- p2))),(Im (p1 + (- p2)))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
((- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (- p2) is complex V12() ext-real Element of REAL
Im (- p2) is complex V12() ext-real Element of REAL
|[(Re (- p2)),(Im (- p2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) + ((- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),(p1),((- p2))) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) + ((- p2)) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 - p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K259((TOP-REAL 2),p1,(- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued V21() V30(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,(- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 + (- p2) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 - p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1 - p2)) is complex Element of COMPLEX
(p1 - p2) `1 is complex V12() ext-real Element of REAL
(p1 - p2) . 1 is complex V12() ext-real Element of REAL
(p1 - p2) `2 is complex V12() ext-real Element of REAL
(p1 - p2) . 2 is complex V12() ext-real Element of REAL
((p1 - p2) `2) * <i> is complex set
((p1 - p2) `1) + (((p1 - p2) `2) * <i>) is complex set
(p2) is complex Element of COMPLEX
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
(p1) - (p2) is complex Element of COMPLEX
((- p2)) is complex Element of COMPLEX
(- p2) `1 is complex V12() ext-real Element of REAL
(- p2) . 1 is complex V12() ext-real Element of REAL
(- p2) `2 is complex V12() ext-real Element of REAL
(- p2) . 2 is complex V12() ext-real Element of REAL
((- p2) `2) * <i> is complex set
((- p2) `1) + (((- p2) `2) * <i>) is complex set
(p1) + ((- p2)) is complex Element of COMPLEX
- (p2) is complex Element of COMPLEX
(p1) + (- (p2)) is complex Element of COMPLEX
0c is empty complex V129() V130() V131() V132() V133() V134() V135() Element of COMPLEX
(0c) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re 0c is complex V12() ext-real Element of REAL
Im 0c is complex V12() ext-real Element of REAL
|[(Re 0c),(Im 0c)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
((0. (TOP-REAL 2))) is complex Element of COMPLEX
(0. (TOP-REAL 2)) `1 is complex V12() ext-real Element of REAL
(0. (TOP-REAL 2)) . 1 is complex V12() ext-real Element of REAL
(0. (TOP-REAL 2)) `2 is complex V12() ext-real Element of REAL
(0. (TOP-REAL 2)) . 2 is complex V12() ext-real Element of REAL
((0. (TOP-REAL 2)) `2) * <i> is complex set
((0. (TOP-REAL 2)) `1) + (((0. (TOP-REAL 2)) `2) * <i>) is complex set
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
p1 is complex set
(p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 is complex V12() ext-real Element of REAL
p2 * p1 is complex set
((p2 * p1)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (p2 * p1) is complex V12() ext-real Element of REAL
Im (p2 * p1) is complex V12() ext-real Element of REAL
|[(Re (p2 * p1)),(Im (p2 * p1))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 * (p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 * (p1) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
(p1) `1 is complex V12() ext-real Element of REAL
(p1) . 1 is complex V12() ext-real Element of REAL
(p1) `2 is complex V12() ext-real Element of REAL
(p1) . 2 is complex V12() ext-real Element of REAL
0 * <i> is complex set
p2 + (0 * <i>) is complex set
Re p2 is complex V12() ext-real Element of REAL
Im p2 is complex V12() ext-real Element of REAL
p2 * (Im p1) is complex V12() ext-real Element of REAL
0 * (Re p1) is complex V12() ext-real Element of REAL
(p2 * (Im p1)) + (0 * (Re p1)) is complex V12() ext-real Element of REAL
p2 * (Re p1) is complex V12() ext-real Element of REAL
0 * (Im p1) is complex V12() ext-real Element of REAL
(p2 * (Re p1)) - (0 * (Im p1)) is complex V12() ext-real Element of REAL
p1 is complex V12() ext-real Element of REAL
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 * p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 * p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1 * p2)) is complex Element of COMPLEX
(p1 * p2) `1 is complex V12() ext-real Element of REAL
(p1 * p2) . 1 is complex V12() ext-real Element of REAL
(p1 * p2) `2 is complex V12() ext-real Element of REAL
(p1 * p2) . 2 is complex V12() ext-real Element of REAL
((p1 * p2) `2) * <i> is complex set
((p1 * p2) `1) + (((p1 * p2) `2) * <i>) is complex set
(p2) is complex Element of COMPLEX
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
p1 * (p2) is complex set
p1 * (p2 `1) is complex V12() ext-real Element of REAL
p1 * (p2 `2) is complex V12() ext-real Element of REAL
|[(p1 * (p2 `1)),(p1 * (p2 `2))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
|.(p1).| is complex V12() ext-real Element of REAL
Re (p1) is complex V12() ext-real Element of REAL
(Re (p1)) ^2 is complex V12() ext-real Element of REAL
Im (p1) is complex V12() ext-real Element of REAL
(Im (p1)) ^2 is complex V12() ext-real Element of REAL
((Re (p1)) ^2) + ((Im (p1)) ^2) is complex V12() ext-real Element of REAL
sqrt (((Re (p1)) ^2) + ((Im (p1)) ^2)) is complex V12() ext-real Element of REAL
(p1 `1) ^2 is complex V12() ext-real Element of REAL
(p1 `2) ^2 is complex V12() ext-real Element of REAL
((p1 `1) ^2) + ((p1 `2) ^2) is complex V12() ext-real Element of REAL
sqrt (((p1 `1) ^2) + ((p1 `2) ^2)) is complex V12() ext-real Element of REAL
p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
len p1 is natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() Element of NAT
|.p1.| is complex V12() ext-real non negative Element of REAL
sqr p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr p1) is complex V12() ext-real Element of REAL
sqrt (Sum (sqr p1)) is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
(p1 . 1) ^2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 . 2) ^2 is complex V12() ext-real Element of REAL
((p1 . 1) ^2) + ((p1 . 2) ^2) is complex V12() ext-real Element of REAL
sqrt (((p1 . 1) ^2) + ((p1 . 2) ^2)) is complex V12() ext-real Element of REAL
(sqr p1) . 1 is complex V12() ext-real Element of REAL
(sqr p1) . 2 is complex V12() ext-real Element of REAL
dom (sqr p1) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom p1 is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
len (sqr p1) is natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len (sqr p1)) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
<*((p1 . 1) ^2),((p1 . 2) ^2)*> is set
<*((p1 . 1) ^2)*> is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
<*((p1 . 2) ^2)*> is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
<*((p1 . 1) ^2)*> ^ <*((p1 . 2) ^2)*> is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (<*((p1 . 1) ^2)*> ^ <*((p1 . 2) ^2)*>) is complex V12() ext-real Element of REAL
Sum <*((p1 . 1) ^2)*> is complex V12() ext-real Element of REAL
(Sum <*((p1 . 1) ^2)*>) + ((p1 . 2) ^2) is complex V12() ext-real Element of REAL
p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
len p1 is natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() Element of NAT
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|.p2.| is complex V12() ext-real non negative Element of REAL
sqr p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr p2) is complex V12() ext-real Element of REAL
sqrt (Sum (sqr p2)) is complex V12() ext-real Element of REAL
|.p1.| is complex V12() ext-real non negative Element of REAL
sqr p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr p1) is complex V12() ext-real Element of REAL
sqrt (Sum (sqr p1)) is complex V12() ext-real Element of REAL
p1 is complex set
(p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|.(p1).| is complex V12() ext-real non negative Element of REAL
sqr (p1) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr (p1)) is complex V12() ext-real Element of REAL
sqrt (Sum (sqr (p1))) is complex V12() ext-real Element of REAL
(Re p1) ^2 is complex V12() ext-real Element of REAL
(Im p1) ^2 is complex V12() ext-real Element of REAL
((Re p1) ^2) + ((Im p1) ^2) is complex V12() ext-real Element of REAL
sqrt (((Re p1) ^2) + ((Im p1) ^2)) is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| `1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| . 1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| `2 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| . 2 is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
|.(p1).| is complex V12() ext-real Element of REAL
Re (p1) is complex V12() ext-real Element of REAL
(Re (p1)) ^2 is complex V12() ext-real Element of REAL
Im (p1) is complex V12() ext-real Element of REAL
(Im (p1)) ^2 is complex V12() ext-real Element of REAL
((Re (p1)) ^2) + ((Im (p1)) ^2) is complex V12() ext-real Element of REAL
sqrt (((Re (p1)) ^2) + ((Im (p1)) ^2)) is complex V12() ext-real Element of REAL
|.p1.| is complex V12() ext-real non negative Element of REAL
sqr p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr p1) is complex V12() ext-real Element of REAL
sqrt (Sum (sqr p1)) is complex V12() ext-real Element of REAL
(p1 `1) ^2 is complex V12() ext-real Element of REAL
(p1 `2) ^2 is complex V12() ext-real Element of REAL
((p1 `1) ^2) + ((p1 `2) ^2) is complex V12() ext-real Element of REAL
sqrt (((p1 `1) ^2) + ((p1 `2) ^2)) is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
Arg (p1) is complex V12() ext-real Element of REAL
p1 is complex Element of COMPLEX
(p1) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re p1 is complex V12() ext-real Element of REAL
Im p1 is complex V12() ext-real Element of REAL
|[(Re p1),(Im p1)]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Arg p1 is complex V12() ext-real Element of REAL
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p2) is complex Element of COMPLEX
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
(p2) is complex V12() ext-real Element of REAL
Arg (p2) is complex V12() ext-real Element of REAL
p1 is complex V12() ext-real Element of REAL
p2 is complex V12() ext-real Element of REAL
|[p1,p2]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|.p3.| is complex V12() ext-real non negative Element of REAL
sqr p3 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr p3) is complex V12() ext-real Element of REAL
sqrt (Sum (sqr p3)) is complex V12() ext-real Element of REAL
(p3) is complex V12() ext-real Element of REAL
(p3) is complex Element of COMPLEX
p3 `1 is complex V12() ext-real Element of REAL
p3 . 1 is complex V12() ext-real Element of REAL
p3 `2 is complex V12() ext-real Element of REAL
p3 . 2 is complex V12() ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
Arg (p3) is complex V12() ext-real Element of REAL
cos (p3) is complex V12() ext-real Element of REAL
|.p3.| * (cos (p3)) is complex V12() ext-real Element of REAL
sin (p3) is complex V12() ext-real Element of REAL
|.p3.| * (sin (p3)) is complex V12() ext-real Element of REAL
|.(p3).| is complex V12() ext-real Element of REAL
Re (p3) is complex V12() ext-real Element of REAL
(Re (p3)) ^2 is complex V12() ext-real Element of REAL
Im (p3) is complex V12() ext-real Element of REAL
(Im (p3)) ^2 is complex V12() ext-real Element of REAL
((Re (p3)) ^2) + ((Im (p3)) ^2) is complex V12() ext-real Element of REAL
sqrt (((Re (p3)) ^2) + ((Im (p3)) ^2)) is complex V12() ext-real Element of REAL
cos (Arg (p3)) is complex V12() ext-real Element of REAL
|.(p3).| * (cos (Arg (p3))) is complex V12() ext-real Element of REAL
sin (Arg (p3)) is complex V12() ext-real Element of REAL
|.(p3).| * (sin (Arg (p3))) is complex V12() ext-real Element of REAL
p2 * <i> is complex set
p1 + (p2 * <i>) is complex set
((p1 + (p2 * <i>))) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (p1 + (p2 * <i>)) is complex V12() ext-real Element of REAL
Im (p1 + (p2 * <i>)) is complex V12() ext-real Element of REAL
|[(Re (p1 + (p2 * <i>))),(Im (p1 + (p2 * <i>)))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
((0. (TOP-REAL 2))) is complex V12() ext-real Element of REAL
Arg ((0. (TOP-REAL 2))) is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex V12() ext-real Element of REAL
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
Arg (p1) is complex V12() ext-real Element of REAL
- p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((- p1)) is complex V12() ext-real Element of REAL
((- p1)) is complex Element of COMPLEX
(- p1) `1 is complex V12() ext-real Element of REAL
(- p1) . 1 is complex V12() ext-real Element of REAL
(- p1) `2 is complex V12() ext-real Element of REAL
(- p1) . 2 is complex V12() ext-real Element of REAL
((- p1) `2) * <i> is complex set
((- p1) `1) + (((- p1) `2) * <i>) is complex set
Arg ((- p1)) is complex V12() ext-real Element of REAL
(p1) + PI is complex V12() ext-real Element of REAL
(p1) - PI is complex V12() ext-real Element of REAL
- (p1) is complex Element of COMPLEX
Arg (- (p1)) is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex V12() ext-real Element of REAL
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
Arg (p1) is complex V12() ext-real Element of REAL
|.p1.| is complex V12() ext-real non negative Element of REAL
sqr p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr p1) is complex V12() ext-real Element of REAL
sqrt (Sum (sqr p1)) is complex V12() ext-real Element of REAL
|[|.p1.|,0]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|.(p1).| is complex V12() ext-real Element of REAL
Re (p1) is complex V12() ext-real Element of REAL
(Re (p1)) ^2 is complex V12() ext-real Element of REAL
Im (p1) is complex V12() ext-real Element of REAL
(Im (p1)) ^2 is complex V12() ext-real Element of REAL
((Re (p1)) ^2) + ((Im (p1)) ^2) is complex V12() ext-real Element of REAL
sqrt (((Re (p1)) ^2) + ((Im (p1)) ^2)) is complex V12() ext-real Element of REAL
0 * <i> is complex set
|.(p1).| + (0 * <i>) is complex set
((|.(p1).| + (0 * <i>))) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
Re (|.(p1).| + (0 * <i>)) is complex V12() ext-real Element of REAL
Im (|.(p1).| + (0 * <i>)) is complex V12() ext-real Element of REAL
|[(Re (|.(p1).| + (0 * <i>))),(Im (|.(p1).| + (0 * <i>)))]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
|[|.(p1).|,0]| is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex V12() ext-real Element of REAL
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
Arg (p1) is complex V12() ext-real Element of REAL
- p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((- p1)) is complex V12() ext-real Element of REAL
((- p1)) is complex Element of COMPLEX
(- p1) `1 is complex V12() ext-real Element of REAL
(- p1) . 1 is complex V12() ext-real Element of REAL
(- p1) `2 is complex V12() ext-real Element of REAL
(- p1) . 2 is complex V12() ext-real Element of REAL
((- p1) `2) * <i> is complex set
((- p1) `1) + (((- p1) `2) * <i>) is complex set
Arg ((- p1)) is complex V12() ext-real Element of REAL
- (p1) is complex Element of COMPLEX
Arg (- (p1)) is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 - p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K259((TOP-REAL 2),p1,(- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued V21() V30(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,(- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 + (- p2) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 - p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1 - p2)) is complex V12() ext-real Element of REAL
((p1 - p2)) is complex Element of COMPLEX
(p1 - p2) `1 is complex V12() ext-real Element of REAL
(p1 - p2) . 1 is complex V12() ext-real Element of REAL
(p1 - p2) `2 is complex V12() ext-real Element of REAL
(p1 - p2) . 2 is complex V12() ext-real Element of REAL
((p1 - p2) `2) * <i> is complex set
((p1 - p2) `1) + (((p1 - p2) `2) * <i>) is complex set
Arg ((p1 - p2)) is complex V12() ext-real Element of REAL
p2 - p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K259((TOP-REAL 2),p2,(- p1)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p2,(- p1)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 + (- p1) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p2 - p1 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p2 - p1)) is complex V12() ext-real Element of REAL
((p2 - p1)) is complex Element of COMPLEX
(p2 - p1) `1 is complex V12() ext-real Element of REAL
(p2 - p1) . 1 is complex V12() ext-real Element of REAL
(p2 - p1) `2 is complex V12() ext-real Element of REAL
(p2 - p1) . 2 is complex V12() ext-real Element of REAL
((p2 - p1) `2) * <i> is complex set
((p2 - p1) `1) + (((p2 - p1) `2) * <i>) is complex set
Arg ((p2 - p1)) is complex V12() ext-real Element of REAL
- (p1 - p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- (p1 - p2) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex V12() ext-real Element of REAL
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
Arg (p1) is complex V12() ext-real Element of REAL
Im (p1) is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex V12() ext-real Element of REAL
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
Arg (p1) is complex V12() ext-real Element of REAL
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p2) is complex V12() ext-real Element of REAL
(p2) is complex Element of COMPLEX
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
Arg (p2) is complex V12() ext-real Element of REAL
p1 + p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued V21() V30(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,p2) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 + p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
((p1 + p2)) is complex V12() ext-real Element of REAL
((p1 + p2)) is complex Element of COMPLEX
(p1 + p2) `1 is complex V12() ext-real Element of REAL
(p1 + p2) . 1 is complex V12() ext-real Element of REAL
(p1 + p2) `2 is complex V12() ext-real Element of REAL
(p1 + p2) . 2 is complex V12() ext-real Element of REAL
((p1 + p2) `2) * <i> is complex set
((p1 + p2) `1) + (((p1 + p2) `2) * <i>) is complex set
Arg ((p1 + p2)) is complex V12() ext-real Element of REAL
(p1) + (p2) is complex Element of COMPLEX
Arg ((p1) + (p2)) is complex V12() ext-real Element of REAL
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p2) is complex Element of COMPLEX
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
p3 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p3) is complex Element of COMPLEX
p3 `1 is complex V12() ext-real Element of REAL
p3 . 1 is complex V12() ext-real Element of REAL
p3 `2 is complex V12() ext-real Element of REAL
p3 . 2 is complex V12() ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((p1),(p2),(p3)) is complex V12() ext-real set
p1 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 - p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
K259((TOP-REAL 2),p1,(- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued V21() V30(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K6(K7(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,(- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p1 + (- p2) is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p1 - p2 is Relation-like NAT -defined REAL -valued V21() FinSequence-like complex-yielding V120() V121() FinSequence of REAL
p3 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
(p1,p2,p3) is complex V12() ext-real Element of REAL
(p1) is complex Element of COMPLEX
p1 `1 is complex V12() ext-real Element of REAL
p1 . 1 is complex V12() ext-real Element of REAL
p1 `2 is complex V12() ext-real Element of REAL
p1 . 2 is complex V12() ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
(p2) is complex Element of COMPLEX
p2 `1 is complex V12() ext-real Element of REAL
p2 . 1 is complex V12() ext-real Element of REAL
p2 `2 is complex V12() ext-real Element of REAL
p2 . 2 is complex V12() ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
(p3) is complex Element of COMPLEX
p3 `1 is complex V12() ext-real Element of REAL
p3 . 1 is complex V12() ext-real Element of REAL
p3 `2 is complex V12() ext-real Element of REAL
p3 . 2 is complex V12() ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((p1),(p2),(p3)) is complex V12() ext-real set
p3 - p2 is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
K259((TOP-REAL 2),p3,(- p2)) is Relation-like V21() V45(2) FinSequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
K493( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p3,(- p2)) is Relation-like