:: EUCLID_3 semantic presentation

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