:: JGRAPH_4 semantic presentation

REAL is non empty V35() V126() V127() V128() V132() set

NAT is V126() V127() V128() V129() V130() V131() V132() Element of K19(REAL)

K19(REAL) is set

COMPLEX is non empty V35() V126() V132() set

RAT is non empty V35() V126() V127() V128() V129() V132() set

INT is non empty V35() V126() V127() V128() V129() V130() V132() set

K20(COMPLEX,COMPLEX) is set

K19(K20(COMPLEX,COMPLEX)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(REAL,REAL) is set

K19(K20(REAL,REAL)) is set

K20(K20(REAL,REAL),REAL) is set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is set

K20(K20(NAT,NAT),NAT) is set

K19(K20(K20(NAT,NAT),NAT)) is set

omega is V126() V127() V128() V129() V130() V131() V132() set

K19(omega) is set

1 is non empty natural V28() real ext-real positive non negative V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT

K20(1,1) is set

K19(K20(1,1)) is set

K20(K20(1,1),1) is set

K19(K20(K20(1,1),1)) is set

K20(K20(1,1),REAL) is set

K19(K20(K20(1,1),REAL)) is set

2 is non empty natural V28() real ext-real positive non negative V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT

K20(2,2) is set

K20(K20(2,2),REAL) is set

K19(K20(K20(2,2),REAL)) is set

K334() is V115() TopStruct

the carrier of K334() is V126() V127() V128() set

RealSpace is strict V115() MetrStruct

R^1 is non empty strict TopSpace-like V115() TopStruct

K19(NAT) is set

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V152() V177() V178() V179() V180() V181() V182() V183() strict V190() V191() L15()

the carrier of (TOP-REAL 2) is functional non empty set

K20( the carrier of (TOP-REAL 2),REAL) is set

K19(K20( the carrier of (TOP-REAL 2),REAL)) is set

K19( the carrier of (TOP-REAL 2)) is set

{} is Function-like functional empty V126() V127() V128() V129() V130() V131() V132() set

0 is Function-like functional empty natural V28() real ext-real non positive non negative V33() V34() V126() V127() V128() V129() V130() V131() V132() Element of NAT

the carrier of R^1 is non empty V126() V127() V128() set

sqrt 0 is V28() real ext-real Element of REAL

sqrt 1 is V28() real ext-real Element of REAL

- 1 is V28() real ext-real non positive set

proj1 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of (TOP-REAL 2),REAL))

proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of (TOP-REAL 2),REAL))

0. (TOP-REAL 2) is Relation-like Function-like V42(2) V51( TOP-REAL 2) V118() V137() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

(0. (TOP-REAL 2)) `1 is V28() real ext-real Element of REAL

(0. (TOP-REAL 2)) `2 is V28() real ext-real Element of REAL

{(0. (TOP-REAL 2))} is functional non empty Element of K19( the carrier of (TOP-REAL 2))

NonZero (TOP-REAL 2) is functional Element of K19( the carrier of (TOP-REAL 2))

[#] (TOP-REAL 2) is functional non empty non proper closed Element of K19( the carrier of (TOP-REAL 2))

{(0. (TOP-REAL 2))} is functional non empty set

([#] (TOP-REAL 2)) \ {(0. (TOP-REAL 2))} is functional Element of K19( the carrier of (TOP-REAL 2))

K19( the carrier of R^1) is set

cn is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.cn.| is V28() real ext-real non negative Element of REAL

cn is non empty TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

K19( the carrier of cn) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Element of K19( the carrier of cn)

p1 is V28() real ext-real set

{ b

{ b

p2 is set

q3 is V28() real ext-real Element of REAL

p2 is V126() V127() V128() Element of K19( the carrier of R^1)

q " p2 is Element of K19( the carrier of cn)

q3 is set

q . q3 is set

VV0 is Element of the carrier of cn

q /. VV0 is V28() real ext-real Element of the carrier of R^1

q . VV0 is V28() real ext-real Element of the carrier of R^1

u2 is V28() real ext-real Element of REAL

[#] R^1 is non empty non proper closed V126() V127() V128() Element of K19( the carrier of R^1)

q3 is set

VV0 is Element of the carrier of cn

q /. VV0 is V28() real ext-real Element of the carrier of R^1

q . VV0 is V28() real ext-real Element of the carrier of R^1

dom q is Element of K19( the carrier of cn)

q . q3 is set

cn is non empty TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

K19( the carrier of cn) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Element of K19( the carrier of cn)

p1 is V28() real ext-real Element of REAL

{ b

{ b

p2 is set

q3 is V28() real ext-real Element of REAL

p2 is V126() V127() V128() Element of K19( the carrier of R^1)

q " p2 is Element of K19( the carrier of cn)

q3 is set

q . q3 is set

VV0 is Element of the carrier of cn

q /. VV0 is V28() real ext-real Element of the carrier of R^1

q . VV0 is V28() real ext-real Element of the carrier of R^1

u2 is V28() real ext-real Element of REAL

[#] R^1 is non empty non proper closed V126() V127() V128() Element of K19( the carrier of R^1)

q3 is set

VV0 is Element of the carrier of cn

q /. VV0 is V28() real ext-real Element of the carrier of R^1

q . VV0 is V28() real ext-real Element of the carrier of R^1

dom q is Element of K19( the carrier of cn)

q . q3 is set

K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set

K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2))) is set

cn is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

rng cn is functional Element of K19( the carrier of (TOP-REAL 2))

cn " is Relation-like Function-like set

dom cn is functional Element of K19( the carrier of (TOP-REAL 2))

q is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

p is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

q . p is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

p1 is functional Element of K19( the carrier of (TOP-REAL 2))

cn . (q . p) is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

p2 is functional non empty closed compact bounded Element of K19( the carrier of (TOP-REAL 2))

cn .: p2 is functional Element of K19( the carrier of (TOP-REAL 2))

q3 is functional Element of K19( the carrier of (TOP-REAL 2))

q3 is functional Element of K19( the carrier of (TOP-REAL 2))

cn | p2 is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

dom (cn | p2) is functional Element of K19( the carrier of (TOP-REAL 2))

(dom cn) /\ p2 is functional Element of K19( the carrier of (TOP-REAL 2))

p1 /\ q3 is functional Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | p2 is non empty strict TopSpace-like T_0 T_1 T_2 compact V195() SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | p2) is non empty set

K19( the carrier of ((TOP-REAL 2) | p2)) is set

(p1 /\ q3) /\ p2 is functional Element of K19( the carrier of (TOP-REAL 2))

VV0 is Element of K19( the carrier of ((TOP-REAL 2) | p2))

[#] ((TOP-REAL 2) | p2) is non empty non proper closed Element of K19( the carrier of ((TOP-REAL 2) | p2))

(p1 /\ q3) /\ ([#] ((TOP-REAL 2) | p2)) is Element of K19( the carrier of ((TOP-REAL 2) | p2))

rng (cn | p2) is functional Element of K19( the carrier of (TOP-REAL 2))

the carrier of (TOP-REAL 2) /\ p2 is functional Element of K19( the carrier of (TOP-REAL 2))

K20( the carrier of ((TOP-REAL 2) | p2), the carrier of (TOP-REAL 2)) is set

K19(K20( the carrier of ((TOP-REAL 2) | p2), the carrier of (TOP-REAL 2))) is set

u3 is Relation-like the carrier of ((TOP-REAL 2) | p2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | p2), the carrier of (TOP-REAL 2)))

(cn | p2) .: p2 is functional Element of K19( the carrier of (TOP-REAL 2))

K20( the carrier of ((TOP-REAL 2) | p2), the carrier of ((TOP-REAL 2) | p2)) is set

K19(K20( the carrier of ((TOP-REAL 2) | p2), the carrier of ((TOP-REAL 2) | p2))) is set

y is Relation-like the carrier of ((TOP-REAL 2) | p2) -defined the carrier of ((TOP-REAL 2) | p2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | p2), the carrier of ((TOP-REAL 2) | p2)))

rng y is Element of K19( the carrier of ((TOP-REAL 2) | p2))

y " is Relation-like Function-like set

dom (y ") is set

rng (y ") is set

dom y is Element of K19( the carrier of ((TOP-REAL 2) | p2))

q4 is Relation-like the carrier of ((TOP-REAL 2) | p2) -defined the carrier of ((TOP-REAL 2) | p2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | p2), the carrier of ((TOP-REAL 2) | p2)))

y " is Relation-like the carrier of ((TOP-REAL 2) | p2) -defined the carrier of ((TOP-REAL 2) | p2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | p2), the carrier of ((TOP-REAL 2) | p2)))

y . (q . p) is set

(y ") . p is set

y . ((y ") . p) is set

y is functional Element of K19( the carrier of (TOP-REAL 2))

u2 is Element of the carrier of ((TOP-REAL 2) | p2)

y is Element of K19( the carrier of ((TOP-REAL 2) | p2))

(y ") .: y is set

q3 /\ p2 is functional Element of K19( the carrier of (TOP-REAL 2))

p1 /\ (q3 /\ p2) is functional Element of K19( the carrier of (TOP-REAL 2))

x is functional Element of K19( the carrier of (TOP-REAL 2))

x /\ ([#] ((TOP-REAL 2) | p2)) is Element of K19( the carrier of ((TOP-REAL 2) | p2))

x /\ q3 is functional Element of K19( the carrier of (TOP-REAL 2))

x is functional Element of K19( the carrier of (TOP-REAL 2))

(cn ") .: y is set

q is set

dom (cn ") is set

K004 is set

(cn ") . K004 is set

cn . q is Relation-like Function-like set

K111 is set

cn . K111 is Relation-like Function-like set

y . q is set

(y ") . K004 is set

x /\ (q3 /\ p2) is functional Element of K19( the carrier of (TOP-REAL 2))

x /\ p2 is functional Element of K19( the carrier of (TOP-REAL 2))

(x /\ p2) /\ q3 is functional Element of K19( the carrier of (TOP-REAL 2))

y /\ q3 is functional Element of K19( the carrier of (TOP-REAL 2))

q .: x is functional Element of K19( the carrier of (TOP-REAL 2))

q .: y is functional Element of K19( the carrier of (TOP-REAL 2))

q .: q3 is functional Element of K19( the carrier of (TOP-REAL 2))

(q .: y) /\ (q .: q3) is functional Element of K19( the carrier of (TOP-REAL 2))

cn " is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

cn is non empty TopSpace-like TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p2 is V28() real ext-real set

p1 is V28() real ext-real set

q3 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

VV0 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

u2 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

u3 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

y is Element of the carrier of cn

VV0 . y is V28() real ext-real Element of the carrier of R^1

y is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

q4 is Element of the carrier of cn

q . q4 is V28() real ext-real Element of the carrier of R^1

p . q4 is V28() real ext-real Element of the carrier of R^1

y . q4 is V28() real ext-real Element of the carrier of R^1

y is V28() real ext-real set

x is V28() real ext-real set

y / x is V28() real ext-real Element of COMPLEX

(y / x) - p1 is V28() real ext-real set

((y / x) - p1) / p2 is V28() real ext-real Element of COMPLEX

VV0 . q4 is V28() real ext-real Element of the carrier of R^1

q3 . q4 is V28() real ext-real Element of the carrier of R^1

u2 . q4 is V28() real ext-real Element of the carrier of R^1

u3 . q4 is V28() real ext-real Element of the carrier of R^1

cn is non empty TopSpace-like TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p2 is V28() real ext-real Element of REAL

p1 is V28() real ext-real Element of REAL

q3 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

VV0 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

u2 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

u3 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

y is Element of the carrier of cn

VV0 . y is V28() real ext-real Element of the carrier of R^1

y is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

q4 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

y is Element of the carrier of cn

q . y is V28() real ext-real Element of the carrier of R^1

p . y is V28() real ext-real Element of the carrier of R^1

q4 . y is V28() real ext-real Element of the carrier of R^1

x is V28() real ext-real Element of REAL

x is V28() real ext-real Element of REAL

x / x is V28() real ext-real Element of COMPLEX

(x / x) - p1 is V28() real ext-real Element of REAL

((x / x) - p1) / p2 is V28() real ext-real Element of COMPLEX

x * (((x / x) - p1) / p2) is V28() real ext-real Element of REAL

u2 . y is V28() real ext-real Element of the carrier of R^1

VV0 . y is V28() real ext-real Element of the carrier of R^1

q3 . y is V28() real ext-real Element of the carrier of R^1

u3 . y is V28() real ext-real Element of the carrier of R^1

y . y is V28() real ext-real Element of the carrier of R^1

cn is non empty TopSpace-like TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p1 is Element of the carrier of cn

q . p1 is V28() real ext-real Element of the carrier of R^1

p2 is V28() real ext-real set

p . p1 is V28() real ext-real Element of the carrier of R^1

p2 ^2 is V28() real ext-real set

p2 * p2 is V28() real ext-real set

cn is non empty TopSpace-like TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p1 is Element of the carrier of cn

p . p1 is V28() real ext-real Element of the carrier of R^1

q . p1 is V28() real ext-real Element of the carrier of R^1

p2 is V28() real ext-real Element of REAL

p2 ^2 is V28() real ext-real Element of REAL

p2 * p2 is V28() real ext-real set

p1 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p2 is Element of the carrier of cn

q . p2 is V28() real ext-real Element of the carrier of R^1

p1 . p2 is V28() real ext-real Element of the carrier of R^1

q3 is V28() real ext-real set

abs q3 is V28() real ext-real Element of REAL

p . p2 is V28() real ext-real Element of the carrier of R^1

q3 ^2 is V28() real ext-real set

q3 * q3 is V28() real ext-real set

sqrt (q3 ^2) is V28() real ext-real set

cn is non empty TopSpace-like TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p1 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p2 is Element of the carrier of cn

q . p2 is V28() real ext-real Element of the carrier of R^1

p1 . p2 is V28() real ext-real Element of the carrier of R^1

q3 is V28() real ext-real set

- q3 is V28() real ext-real set

p . p2 is V28() real ext-real Element of the carrier of R^1

0 - q3 is V28() real ext-real Element of REAL

cn is non empty TopSpace-like TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p2 is V28() real ext-real set

p1 is V28() real ext-real set

q3 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

VV0 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

u2 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

u3 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

y is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

q4 is Element of the carrier of cn

y . q4 is V28() real ext-real Element of the carrier of R^1

u3 . q4 is V28() real ext-real Element of the carrier of R^1

y is V28() real ext-real Element of REAL

abs y is V28() real ext-real Element of REAL

q4 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

y is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

x is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

x is Element of the carrier of cn

q . x is V28() real ext-real Element of the carrier of R^1

p . x is V28() real ext-real Element of the carrier of R^1

x . x is V28() real ext-real Element of the carrier of R^1

q is V28() real ext-real set

K004 is V28() real ext-real set

q / K004 is V28() real ext-real Element of COMPLEX

(q / K004) - p1 is V28() real ext-real set

((q / K004) - p1) / p2 is V28() real ext-real Element of COMPLEX

(((q / K004) - p1) / p2) ^2 is V28() real ext-real Element of COMPLEX

(((q / K004) - p1) / p2) * (((q / K004) - p1) / p2) is V28() real ext-real set

1 - ((((q / K004) - p1) / p2) ^2) is V28() real ext-real Element of REAL

abs (1 - ((((q / K004) - p1) / p2) ^2)) is V28() real ext-real Element of REAL

sqrt (abs (1 - ((((q / K004) - p1) / p2) ^2))) is V28() real ext-real Element of REAL

- (sqrt (abs (1 - ((((q / K004) - p1) / p2) ^2)))) is V28() real ext-real Element of REAL

K004 * (- (sqrt (abs (1 - ((((q / K004) - p1) / p2) ^2))))) is V28() real ext-real Element of REAL

u2 . x is V28() real ext-real Element of the carrier of R^1

q3 . x is V28() real ext-real Element of the carrier of R^1

VV0 . x is V28() real ext-real Element of the carrier of R^1

u3 . x is V28() real ext-real Element of the carrier of R^1

y . x is V28() real ext-real Element of the carrier of R^1

q4 . x is V28() real ext-real Element of the carrier of R^1

y . x is V28() real ext-real Element of the carrier of R^1

cn is non empty TopSpace-like TopStruct

the carrier of cn is non empty set

K20( the carrier of cn, the carrier of R^1) is set

K19(K20( the carrier of cn, the carrier of R^1)) is set

q is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

p2 is V28() real ext-real set

p1 is V28() real ext-real set

q3 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

VV0 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

u2 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

u3 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

y is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

q4 is Element of the carrier of cn

y . q4 is V28() real ext-real Element of the carrier of R^1

u3 . q4 is V28() real ext-real Element of the carrier of R^1

y is V28() real ext-real Element of REAL

abs y is V28() real ext-real Element of REAL

q4 is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

y is Relation-like the carrier of cn -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of cn, the carrier of R^1))

x is Element of the carrier of cn

q . x is V28() real ext-real Element of the carrier of R^1

p . x is V28() real ext-real Element of the carrier of R^1

y . x is V28() real ext-real Element of the carrier of R^1

x is V28() real ext-real set

q is V28() real ext-real set

x / q is V28() real ext-real Element of COMPLEX

(x / q) - p1 is V28() real ext-real set

((x / q) - p1) / p2 is V28() real ext-real Element of COMPLEX

(((x / q) - p1) / p2) ^2 is V28() real ext-real Element of COMPLEX

(((x / q) - p1) / p2) * (((x / q) - p1) / p2) is V28() real ext-real set

1 - ((((x / q) - p1) / p2) ^2) is V28() real ext-real Element of REAL

abs (1 - ((((x / q) - p1) / p2) ^2)) is V28() real ext-real Element of REAL

sqrt (abs (1 - ((((x / q) - p1) / p2) ^2))) is V28() real ext-real Element of REAL

q * (sqrt (abs (1 - ((((x / q) - p1) / p2) ^2)))) is V28() real ext-real Element of REAL

u2 . x is V28() real ext-real Element of the carrier of R^1

q3 . x is V28() real ext-real Element of the carrier of R^1

VV0 . x is V28() real ext-real Element of the carrier of R^1

u3 . x is V28() real ext-real Element of the carrier of R^1

y . x is V28() real ext-real Element of the carrier of R^1

q4 . x is V28() real ext-real Element of the carrier of R^1

cn is natural V28() real ext-real set

TOP-REAL cn is non empty TopSpace-like T_0 T_1 T_2 V152() V177() V178() V179() V180() V181() V182() V183() strict V190() V191() L15()

the carrier of (TOP-REAL cn) is functional non empty set

K20( the carrier of (TOP-REAL cn), the carrier of R^1) is set

K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1)) is set

q is Relation-like Function-like V42(cn) V118() V137() Element of the carrier of (TOP-REAL cn)

|.q.| is V28() real ext-real non negative Element of REAL

cn is natural V28() real ext-real set

TOP-REAL cn is non empty TopSpace-like T_0 T_1 T_2 V152() V177() V178() V179() V180() V181() V182() V183() strict V190() V191() L15()

the carrier of (TOP-REAL cn) is functional non empty set

(cn) is Relation-like the carrier of (TOP-REAL cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1))

K20( the carrier of (TOP-REAL cn), the carrier of R^1) is set

K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1)) is set

dom (cn) is functional Element of K19( the carrier of (TOP-REAL cn))

K19( the carrier of (TOP-REAL cn)) is set

REAL cn is non empty V139() M17( REAL )

cn is natural V28() real ext-real set

TOP-REAL cn is non empty TopSpace-like T_0 T_1 T_2 V152() V177() V178() V179() V180() V181() V182() V183() strict V190() V191() L15()

(cn) is Relation-like the carrier of (TOP-REAL cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1))

the carrier of (TOP-REAL cn) is functional non empty set

K20( the carrier of (TOP-REAL cn), the carrier of R^1) is set

K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1)) is set

q is Relation-like Function-like V42(cn) V118() V137() Element of the carrier of (TOP-REAL cn)

(cn) . q is V28() real ext-real Element of the carrier of R^1

|.q.| is V28() real ext-real non negative Element of REAL

cn is natural V28() real ext-real set

TOP-REAL cn is non empty TopSpace-like T_0 T_1 T_2 V152() V177() V178() V179() V180() V181() V182() V183() strict V190() V191() L15()

(cn) is Relation-like the carrier of (TOP-REAL cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1))

the carrier of (TOP-REAL cn) is functional non empty set

K20( the carrier of (TOP-REAL cn), the carrier of R^1) is set

K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1)) is set

cn is natural V28() real ext-real V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT

TOP-REAL cn is non empty TopSpace-like T_0 T_1 T_2 V152() V177() V178() V179() V180() V181() V182() V183() strict V190() V191() L15()

the carrier of (TOP-REAL cn) is functional non empty set

K19( the carrier of (TOP-REAL cn)) is set

(cn) is Relation-like the carrier of (TOP-REAL cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1))

K20( the carrier of (TOP-REAL cn), the carrier of R^1) is set

K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1)) is set

q is functional Element of K19( the carrier of (TOP-REAL cn))

(TOP-REAL cn) | q is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL cn

the carrier of ((TOP-REAL cn) | q) is set

K20( the carrier of ((TOP-REAL cn) | q), the carrier of R^1) is set

K19(K20( the carrier of ((TOP-REAL cn) | q), the carrier of R^1)) is set

p is Relation-like the carrier of ((TOP-REAL cn) | q) -defined the carrier of R^1 -valued Function-like total quasi_total Element of K19(K20( the carrier of ((TOP-REAL cn) | q), the carrier of R^1))

the carrier of (TOP-REAL cn) /\ q is functional Element of K19( the carrier of (TOP-REAL cn))

dom p is Element of K19( the carrier of ((TOP-REAL cn) | q))

K19( the carrier of ((TOP-REAL cn) | q)) is set

p2 is set

p . p2 is set

(cn) . p2 is set

dom (cn) is functional Element of K19( the carrier of (TOP-REAL cn))

(dom (cn)) /\ q is functional Element of K19( the carrier of (TOP-REAL cn))

p1 is Relation-like the carrier of (TOP-REAL cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1))

p1 | q is Relation-like the carrier of (TOP-REAL cn) -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of (TOP-REAL cn), the carrier of R^1))

cn is natural V28() real ext-real V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT

Euclid cn is non empty strict Reflexive discerning V85() triangle MetrStruct

the carrier of (Euclid cn) is non empty set

TOP-REAL cn is non empty TopSpace-like T_0 T_1 T_2 V152() V177() V178() V179() V180() V181() V182() V183() strict V190() V191() L15()

the carrier of (TOP-REAL cn) is functional non empty set

K19( the carrier of (TOP-REAL cn)) is set

q is Element of the carrier of (Euclid cn)

p is V28() real ext-real Element of REAL

cl_Ball (q,p) is Element of K19( the carrier of (Euclid cn))

K19( the carrier of (Euclid cn)) is set

p1 is functional Element of K19( the carrier of (TOP-REAL cn))

p + 1 is V28() real ext-real Element of REAL

Ball (q,(p + 1)) is bounded Element of K19( the carrier of (Euclid cn))

p2 is set

q3 is Element of the carrier of (Euclid cn)

dist (q,q3) is V28() real ext-real Element of REAL

the topology of (TOP-REAL cn) is non empty open Element of K19(K19( the carrier of (TOP-REAL cn)))

K19(K19( the carrier of (TOP-REAL cn))) is set

TopStruct(# the carrier of (TOP-REAL cn), the topology of (TOP-REAL cn) #) is non empty strict TopSpace-like TopStruct

TopSpaceMetr (Euclid cn) is TopStruct

Family_open_set (Euclid cn) is Element of K19(K19( the carrier of (Euclid cn)))

K19(K19( the carrier of (Euclid cn))) is set

TopStruct(# the carrier of (Euclid cn),(Family_open_set (Euclid cn)) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr (Euclid cn)) is set

K19( the carrier of (TopSpaceMetr (Euclid cn))) is set

p2 is Element of K19( the carrier of (TopSpaceMetr (Euclid cn)))

Euclid 2 is non empty strict Reflexive discerning V85() triangle MetrStruct

the carrier of (Euclid 2) is non empty set

cn is Element of the carrier of (Euclid 2)

q is V28() real ext-real Element of REAL

cl_Ball (cn,q) is Element of K19( the carrier of (Euclid 2))

K19( the carrier of (Euclid 2)) is set

p is functional Element of K19( the carrier of (TOP-REAL 2))

cn is V28() real ext-real set

q is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

q `2 is V28() real ext-real Element of REAL

|.q.| is V28() real ext-real non negative Element of REAL

(q `2) / |.q.| is V28() real ext-real Element of COMPLEX

q `1 is V28() real ext-real Element of REAL

((q `2) / |.q.|) - cn is V28() real ext-real set

1 - cn is V28() real ext-real Element of REAL

(((q `2) / |.q.|) - cn) / (1 - cn) is V28() real ext-real Element of COMPLEX

((((q `2) / |.q.|) - cn) / (1 - cn)) ^2 is V28() real ext-real Element of COMPLEX

((((q `2) / |.q.|) - cn) / (1 - cn)) * ((((q `2) / |.q.|) - cn) / (1 - cn)) is V28() real ext-real set

1 - (((((q `2) / |.q.|) - cn) / (1 - cn)) ^2) is V28() real ext-real Element of REAL

sqrt (1 - (((((q `2) / |.q.|) - cn) / (1 - cn)) ^2)) is V28() real ext-real Element of REAL

- (sqrt (1 - (((((q `2) / |.q.|) - cn) / (1 - cn)) ^2))) is V28() real ext-real Element of REAL

|[(- (sqrt (1 - (((((q `2) / |.q.|) - cn) / (1 - cn)) ^2)))),((((q `2) / |.q.|) - cn) / (1 - cn))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.q.| * |[(- (sqrt (1 - (((((q `2) / |.q.|) - cn) / (1 - cn)) ^2)))),((((q `2) / |.q.|) - cn) / (1 - cn))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

1 + cn is V28() real ext-real Element of REAL

(((q `2) / |.q.|) - cn) / (1 + cn) is V28() real ext-real Element of COMPLEX

((((q `2) / |.q.|) - cn) / (1 + cn)) ^2 is V28() real ext-real Element of COMPLEX

((((q `2) / |.q.|) - cn) / (1 + cn)) * ((((q `2) / |.q.|) - cn) / (1 + cn)) is V28() real ext-real set

1 - (((((q `2) / |.q.|) - cn) / (1 + cn)) ^2) is V28() real ext-real Element of REAL

sqrt (1 - (((((q `2) / |.q.|) - cn) / (1 + cn)) ^2)) is V28() real ext-real Element of REAL

- (sqrt (1 - (((((q `2) / |.q.|) - cn) / (1 + cn)) ^2))) is V28() real ext-real Element of REAL

|[(- (sqrt (1 - (((((q `2) / |.q.|) - cn) / (1 + cn)) ^2)))),((((q `2) / |.q.|) - cn) / (1 + cn))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.q.| * |[(- (sqrt (1 - (((((q `2) / |.q.|) - cn) / (1 + cn)) ^2)))),((((q `2) / |.q.|) - cn) / (1 + cn))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

p is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

cn is V28() real ext-real set

cn is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

cn `2 is V28() real ext-real Element of REAL

|.cn.| is V28() real ext-real non negative Element of REAL

(cn `2) / |.cn.| is V28() real ext-real Element of COMPLEX

cn `1 is V28() real ext-real Element of REAL

q is V28() real ext-real set

(q) is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

(q) . cn is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

((cn `2) / |.cn.|) - q is V28() real ext-real set

1 - q is V28() real ext-real Element of REAL

(((cn `2) / |.cn.|) - q) / (1 - q) is V28() real ext-real Element of COMPLEX

((((cn `2) / |.cn.|) - q) / (1 - q)) ^2 is V28() real ext-real Element of COMPLEX

((((cn `2) / |.cn.|) - q) / (1 - q)) * ((((cn `2) / |.cn.|) - q) / (1 - q)) is V28() real ext-real set

1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2) is V28() real ext-real Element of REAL

sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2)) is V28() real ext-real Element of REAL

- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2))) is V28() real ext-real Element of REAL

|.cn.| * (- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2)))) is V28() real ext-real Element of REAL

|.cn.| * ((((cn `2) / |.cn.|) - q) / (1 - q)) is V28() real ext-real Element of REAL

|[(|.cn.| * (- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2))))),(|.cn.| * ((((cn `2) / |.cn.|) - q) / (1 - q)))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

(q,cn) is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|[(- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2)))),((((cn `2) / |.cn.|) - q) / (1 - q))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.cn.| * |[(- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2)))),((((cn `2) / |.cn.|) - q) / (1 - q))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

cn is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

cn `2 is V28() real ext-real Element of REAL

|.cn.| is V28() real ext-real non negative Element of REAL

(cn `2) / |.cn.| is V28() real ext-real Element of COMPLEX

cn `1 is V28() real ext-real Element of REAL

q is V28() real ext-real Element of REAL

(q) is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

(q) . cn is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

((cn `2) / |.cn.|) - q is V28() real ext-real Element of REAL

1 + q is V28() real ext-real Element of REAL

(((cn `2) / |.cn.|) - q) / (1 + q) is V28() real ext-real Element of COMPLEX

((((cn `2) / |.cn.|) - q) / (1 + q)) ^2 is V28() real ext-real Element of COMPLEX

((((cn `2) / |.cn.|) - q) / (1 + q)) * ((((cn `2) / |.cn.|) - q) / (1 + q)) is V28() real ext-real set

1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2) is V28() real ext-real Element of REAL

sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2)) is V28() real ext-real Element of REAL

- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2))) is V28() real ext-real Element of REAL

|.cn.| * (- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2)))) is V28() real ext-real Element of REAL

|.cn.| * ((((cn `2) / |.cn.|) - q) / (1 + q)) is V28() real ext-real Element of REAL

|[(|.cn.| * (- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2))))),(|.cn.| * ((((cn `2) / |.cn.|) - q) / (1 + q)))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

(q,cn) is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|[(- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2)))),((((cn `2) / |.cn.|) - q) / (1 + q))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.cn.| * |[(- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2)))),((((cn `2) / |.cn.|) - q) / (1 + q))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

1 - q is V28() real ext-real Element of REAL

(((cn `2) / |.cn.|) - q) / (1 - q) is V28() real ext-real Element of COMPLEX

- 1 is V28() real ext-real non positive Element of REAL

cn is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

cn `2 is V28() real ext-real Element of REAL

|.cn.| is V28() real ext-real non negative Element of REAL

(cn `2) / |.cn.| is V28() real ext-real Element of COMPLEX

cn `1 is V28() real ext-real Element of REAL

q is V28() real ext-real Element of REAL

(q) is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

(q) . cn is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

((cn `2) / |.cn.|) - q is V28() real ext-real Element of REAL

1 - q is V28() real ext-real Element of REAL

(((cn `2) / |.cn.|) - q) / (1 - q) is V28() real ext-real Element of COMPLEX

((((cn `2) / |.cn.|) - q) / (1 - q)) ^2 is V28() real ext-real Element of COMPLEX

((((cn `2) / |.cn.|) - q) / (1 - q)) * ((((cn `2) / |.cn.|) - q) / (1 - q)) is V28() real ext-real set

1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2) is V28() real ext-real Element of REAL

sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2)) is V28() real ext-real Element of REAL

- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2))) is V28() real ext-real Element of REAL

|.cn.| * (- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2)))) is V28() real ext-real Element of REAL

|.cn.| * ((((cn `2) / |.cn.|) - q) / (1 - q)) is V28() real ext-real Element of REAL

|[(|.cn.| * (- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2))))),(|.cn.| * ((((cn `2) / |.cn.|) - q) / (1 - q)))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

1 + q is V28() real ext-real Element of REAL

(((cn `2) / |.cn.|) - q) / (1 + q) is V28() real ext-real Element of COMPLEX

((((cn `2) / |.cn.|) - q) / (1 + q)) ^2 is V28() real ext-real Element of COMPLEX

((((cn `2) / |.cn.|) - q) / (1 + q)) * ((((cn `2) / |.cn.|) - q) / (1 + q)) is V28() real ext-real set

1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2) is V28() real ext-real Element of REAL

sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2)) is V28() real ext-real Element of REAL

- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2))) is V28() real ext-real Element of REAL

|.cn.| * (- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2)))) is V28() real ext-real Element of REAL

|.cn.| * ((((cn `2) / |.cn.|) - q) / (1 + q)) is V28() real ext-real Element of REAL

|[(|.cn.| * (- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 + q)) ^2))))),(|.cn.| * ((((cn `2) / |.cn.|) - q) / (1 + q)))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

(q,cn) is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|[(- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2)))),((((cn `2) / |.cn.|) - q) / (1 - q))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.cn.| * |[(- (sqrt (1 - (((((cn `2) / |.cn.|) - q) / (1 - q)) ^2)))),((((cn `2) / |.cn.|) - q) / (1 - q))]| is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.cn.| ^2 is V28() real ext-real Element of REAL

|.cn.| * |.cn.| is V28() real ext-real non negative set

(cn `1) ^2 is V28() real ext-real Element of REAL

(cn `1) * (cn `1) is V28() real ext-real set

(cn `2) ^2 is V28() real ext-real Element of REAL

(cn `2) * (cn `2) is V28() real ext-real set

((cn `1) ^2) + ((cn `2) ^2) is V28() real ext-real Element of REAL

((cn `2) ^2) / (|.cn.| ^2) is V28() real ext-real Element of COMPLEX

1 ^2 is V28() real ext-real Element of REAL

1 * 1 is V28() real ext-real non negative set

((cn `2) / |.cn.|) ^2 is V28() real ext-real Element of COMPLEX

((cn `2) / |.cn.|) * ((cn `2) / |.cn.|) is V28() real ext-real set

sqrt (((cn `2) / |.cn.|) ^2) is V28() real ext-real set

- ((cn `2) / |.cn.|) is V28() real ext-real Element of COMPLEX

sqrt (|.cn.| ^2) is V28() real ext-real Element of REAL

1 * |.cn.| is V28() real ext-real non negative Element of REAL

((cn `2) / |.cn.|) * |.cn.| is V28() real ext-real Element of REAL

|.cn.| ^2 is V28() real ext-real Element of REAL

|.cn.| * |.cn.| is V28() real ext-real non negative set

(cn `1) ^2 is V28() real ext-real Element of REAL

(cn `1) * (cn `1) is V28() real ext-real set

(cn `2) ^2 is V28() real ext-real Element of REAL

(cn `2) * (cn `2) is V28() real ext-real set

((cn `1) ^2) + ((cn `2) ^2) is V28() real ext-real Element of REAL

- |.cn.| is V28() real ext-real non positive Element of REAL

- (1 + q) is V28() real ext-real Element of REAL

(- (1 + q)) / (1 + q) is V28() real ext-real Element of COMPLEX

- (cn `2) is V28() real ext-real Element of REAL

cn is functional non empty Element of K19( the carrier of (TOP-REAL 2))

proj1 | cn is Relation-like the carrier of ((TOP-REAL 2) | cn) -defined REAL -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | cn),REAL))

(TOP-REAL 2) | cn is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | cn) is non empty set

K20( the carrier of ((TOP-REAL 2) | cn),REAL) is set

K19(K20( the carrier of ((TOP-REAL 2) | cn),REAL)) is set

K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1) is set

K19(K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1)) is set

q is Relation-like the carrier of ((TOP-REAL 2) | cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1))

p is Element of the carrier of ((TOP-REAL 2) | cn)

q . p is V28() real ext-real Element of the carrier of R^1

proj1 . p is set

dom proj1 is functional Element of K19( the carrier of (TOP-REAL 2))

(dom proj1) /\ cn is functional Element of K19( the carrier of (TOP-REAL 2))

p is Element of the carrier of ((TOP-REAL 2) | cn)

(proj1 | cn) . p is V28() real ext-real Element of REAL

proj1 . p is set

cn is functional non empty Element of K19( the carrier of (TOP-REAL 2))

proj2 | cn is Relation-like the carrier of ((TOP-REAL 2) | cn) -defined REAL -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | cn),REAL))

(TOP-REAL 2) | cn is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | cn) is non empty set

K20( the carrier of ((TOP-REAL 2) | cn),REAL) is set

K19(K20( the carrier of ((TOP-REAL 2) | cn),REAL)) is set

K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1) is set

K19(K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1)) is set

q is Relation-like the carrier of ((TOP-REAL 2) | cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1))

p is Element of the carrier of ((TOP-REAL 2) | cn)

q . p is V28() real ext-real Element of the carrier of R^1

proj2 . p is set

dom proj2 is functional Element of K19( the carrier of (TOP-REAL 2))

(dom proj2) /\ cn is functional Element of K19( the carrier of (TOP-REAL 2))

p is Element of the carrier of ((TOP-REAL 2) | cn)

(proj2 | cn) . p is V28() real ext-real Element of REAL

proj2 . p is set

(2) is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of R^1))

K20( the carrier of (TOP-REAL 2), the carrier of R^1) is set

K19(K20( the carrier of (TOP-REAL 2), the carrier of R^1)) is set

dom (2) is functional Element of K19( the carrier of (TOP-REAL 2))

cn is functional non empty Element of K19( the carrier of (TOP-REAL 2))

(2) | cn is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of R^1))

(TOP-REAL 2) | cn is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | cn) is non empty set

K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1) is set

K19(K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1)) is set

q is Relation-like the carrier of ((TOP-REAL 2) | cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1))

p is Element of the carrier of ((TOP-REAL 2) | cn)

q . p is V28() real ext-real Element of the carrier of R^1

(2) . p is set

(dom (2)) /\ cn is functional Element of K19( the carrier of (TOP-REAL 2))

p is Element of the carrier of ((TOP-REAL 2) | cn)

((2) | cn) . p is set

(2) . p is set

cn is functional non empty Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | cn is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | cn) is non empty set

K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1) is set

K19(K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1)) is set

(2) | cn is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of R^1))

q is Relation-like the carrier of ((TOP-REAL 2) | cn) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | cn), the carrier of R^1))

p is Element of the carrier of ((TOP-REAL 2) | cn)

q . p is V28() real ext-real Element of the carrier of R^1

(2) . p is set

p1 is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.p1.| is V28() real ext-real non negative Element of REAL

cn is V28() real ext-real Element of REAL

1 - cn is V28() real ext-real Element of REAL

q is functional non empty Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | q is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | q) is non empty set

K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1) is set

K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1)) is set

p is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

(2) | q is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of R^1))

proj2 | q is Relation-like the carrier of ((TOP-REAL 2) | q) -defined REAL -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q),REAL))

K20( the carrier of ((TOP-REAL 2) | q),REAL) is set

K19(K20( the carrier of ((TOP-REAL 2) | q),REAL)) is set

u2 is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

p1 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

u2 is Element of the carrier of ((TOP-REAL 2) | q)

p1 . u2 is V28() real ext-real Element of the carrier of R^1

VV0 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

u2 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

dom u2 is Element of K19( the carrier of ((TOP-REAL 2) | q))

K19( the carrier of ((TOP-REAL 2) | q)) is set

dom p is Element of K19( the carrier of ((TOP-REAL 2) | q))

u3 is set

p . u3 is set

u2 . u3 is set

q4 is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

proj2 . q4 is V28() real ext-real Element of REAL

q4 `2 is V28() real ext-real Element of REAL

(2) . q4 is V28() real ext-real Element of the carrier of R^1

|.q4.| is V28() real ext-real non negative Element of REAL

y is Element of the carrier of ((TOP-REAL 2) | q)

VV0 . y is V28() real ext-real Element of the carrier of R^1

proj2 . y is set

p1 . y is V28() real ext-real Element of the carrier of R^1

(2) . y is set

p . q4 is set

(q4 `2) / |.q4.| is V28() real ext-real Element of COMPLEX

((q4 `2) / |.q4.|) - cn is V28() real ext-real Element of REAL

(((q4 `2) / |.q4.|) - cn) / (1 - cn) is V28() real ext-real Element of COMPLEX

|.q4.| * ((((q4 `2) / |.q4.|) - cn) / (1 - cn)) is V28() real ext-real Element of REAL

cn is V28() real ext-real Element of REAL

1 + cn is V28() real ext-real Element of REAL

q is functional non empty Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | q is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | q) is non empty set

K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1) is set

K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1)) is set

p is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

(2) | q is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of R^1))

proj2 | q is Relation-like the carrier of ((TOP-REAL 2) | q) -defined REAL -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q),REAL))

K20( the carrier of ((TOP-REAL 2) | q),REAL) is set

K19(K20( the carrier of ((TOP-REAL 2) | q),REAL)) is set

u2 is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

p1 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

u2 is Element of the carrier of ((TOP-REAL 2) | q)

p1 . u2 is V28() real ext-real Element of the carrier of R^1

VV0 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

u2 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

dom u2 is Element of K19( the carrier of ((TOP-REAL 2) | q))

K19( the carrier of ((TOP-REAL 2) | q)) is set

dom p is Element of K19( the carrier of ((TOP-REAL 2) | q))

u3 is set

p . u3 is set

u2 . u3 is set

q4 is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

proj2 . q4 is V28() real ext-real Element of REAL

q4 `2 is V28() real ext-real Element of REAL

(2) . q4 is V28() real ext-real Element of the carrier of R^1

|.q4.| is V28() real ext-real non negative Element of REAL

y is Element of the carrier of ((TOP-REAL 2) | q)

VV0 . y is V28() real ext-real Element of the carrier of R^1

proj2 . y is set

p1 . y is V28() real ext-real Element of the carrier of R^1

(2) . y is set

p . q4 is set

(q4 `2) / |.q4.| is V28() real ext-real Element of COMPLEX

((q4 `2) / |.q4.|) - cn is V28() real ext-real Element of REAL

(((q4 `2) / |.q4.|) - cn) / (1 + cn) is V28() real ext-real Element of COMPLEX

|.q4.| * ((((q4 `2) / |.q4.|) - cn) / (1 + cn)) is V28() real ext-real Element of REAL

cn is V28() real ext-real Element of REAL

1 - cn is V28() real ext-real Element of REAL

q is functional non empty Element of K19( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | q is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | q) is non empty set

K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1) is set

K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1)) is set

p is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

(2) | q is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of R^1))

proj2 | q is Relation-like the carrier of ((TOP-REAL 2) | q) -defined REAL -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q),REAL))

K20( the carrier of ((TOP-REAL 2) | q),REAL) is set

K19(K20( the carrier of ((TOP-REAL 2) | q),REAL)) is set

u2 is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

p1 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

u2 is Element of the carrier of ((TOP-REAL 2) | q)

p1 . u2 is V28() real ext-real Element of the carrier of R^1

VV0 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

u2 is Relation-like the carrier of ((TOP-REAL 2) | q) -defined the carrier of R^1 -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of ((TOP-REAL 2) | q), the carrier of R^1))

dom u2 is Element of K19( the carrier of ((TOP-REAL 2) | q))

K19( the carrier of ((TOP-REAL 2) | q)) is set

dom p is Element of K19( the carrier of ((TOP-REAL 2) | q))

u3 is set

p . u3 is set

u2 . u3 is set

y is Relation-like Function-like V42(2) V118() V137() Element of the carrier of (TOP-REAL 2)

|.y.| is V28() real ext-real non negative Element of REAL

|.y.| ^2 is V28() real ext-real Element of REAL

|.y.| * |.y.| is V28() real ext-real non negative set

y `1 is V28() real ext-real Element of REAL

(y `1) ^2 is V28() real ext-real Element of REAL

(y `1) * (y `1) is V28() real ext-real set

y `2 is V28() real ext-real Element of REAL

(y `2) ^2 is V28() real ext-real Element of REAL

(y `2) * (y `2) is V28() real ext-real set

((y `1) ^2) + ((y `2) ^2) is V28() real ext-real Element of REAL

(y `2) - |.y.| is V28() real ext-real Element of REAL

(y `2) + |.y.| is V28() real ext-real Element of REAL

((y `2) - |.y.|) * ((y `2) + |.y.|) is V28() real ext-real Element of REAL

- ((y `1) ^2) is V28() real ext-real Element of REAL

(y `2) / |.y.| is V28() real ext-real Element of COMPLEX

|.y.| / |.y.| is V28() real ext-real non negative Element of COMPLEX

((y `2) / |.y.|) - cn is V28() real ext-real Element of REAL

(1 - cn) ^2 is V28() real ext-real Element of REAL

(1 - cn) * (1 - cn) is V28() real ext-real set

(1 - cn) + cn is V28() real ext-real Element of REAL

0 + cn is V28() real ext-real Element of REAL

cn - ((y `2) / |.y.|) is V28() real ext-real Element of REAL

- (1 - cn) is V28() real ext-real Element of REAL

- (cn - ((y `2) / |.y.|)) is V28() real ext-real Element of REAL

(((y `2) / |.y.|) - cn) ^2 is V28() real ext-real Element of REAL

(((y `2) / |.y.|) - cn) * (((y `2) / |.y.|) - cn) is V28() real ext-real set

((((y `2) / |.y.|) - cn) ^2) / ((1 - cn) ^2) is V28() real ext-real Element of COMPLEX

((1 - cn) ^2) / ((1 - cn) ^2) is V28() real ext-real Element of COMPLEX

(((y `2) / |.y.|) - cn) / (1 - cn) is V28() real ext-real Element of COMPLEX

((((y `2) / |.y.|) - cn) / (1 - cn)) ^2 is V28() real ext-real Element of COMPLEX

((((y `2) / |.y.|) - cn) / (1 - cn)) * ((((y `2) / |.y.|) - cn) / (1 - cn)) is V28() real ext-real set

1 - (((((y `2) / |.y.|) - cn) / (1 - cn)) ^2) is V28() real ext-real Element of REAL

abs (1 - (((((y `2) / |.y.|) - cn) / (1 - cn)) ^2)) is V28() real ext-real Element of REAL

p . y is set

sqrt (abs (1 - (((((y `2) / |.y.|) - cn) / (1 - cn)) ^2))) is V28() real ext-real Element of REAL

- (sqrt (abs (1 - (((((y `2) / |.y.|) - cn) / (1 - cn)) ^2)))) is V28() real ext-real Element of REAL

|.y.| * (- (sqrt (abs (1 - (((((y `2) / |.y.|) - cn) / (1 - cn)) ^2))))) is V28() real ext-real Element of REAL

proj2 . y is V28() real ext-real Element of REAL

(2) . y is V28() real ext-real Element of the carrier of R^1

q4 is Element of the carrier of ((TOP-REAL 2) | q)

VV0 . q4 is V28() real ext-real Element of the carrier of R^1

proj2 . q4 is set

p1 . q4 is V28() real ext-real Element of the carrier of R^1

(2) . q4 is set

cn is V28() real ext-real Element of REAL

1 + cn is V28() real ext-real Element of