:: 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₁ where b₁ is Element of the carrier of cn : not q /. b₁ <= p1 } is set
{ b₁ where b₁ is V28() real ext-real Element of REAL : not b₁ <= p1 } is set
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₁ where b₁ is Element of the carrier of cn : not p1 <= q /. b₁ } is set
{ b₁ where b₁ is V28() real ext-real Element of REAL : not p1 <= b₁ } is set
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