REAL is non empty V36() V88() V171() V172() V173() V177() V213() V214() V216() set
NAT is V88() V171() V172() V173() V174() V175() V176() V177() V213() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V36() V171() V177() set
omega is V88() V171() V172() V173() V174() V175() V176() V177() V213() set
K19(omega) is set
K19(NAT) is set
K281() is non empty strict TopSpace-like V122() TopStruct
the carrier of K281() is non empty V171() V172() V173() set
1 is non empty natural V28() real ext-real positive non negative V123() V124() V171() V172() V173() V174() V175() V176() V211() V213() Element of NAT
INT is non empty V36() V171() V172() V173() V174() V175() V177() set
K20(1,1) is RAT -valued INT -valued V161() V162() V163() V164() set
RAT is non empty V36() V171() V172() V173() V174() V177() set
K19(K20(1,1)) is set
K20(K20(1,1),1) is RAT -valued INT -valued V161() V162() V163() V164() set
K19(K20(K20(1,1),1)) is set
K20(K20(1,1),REAL) is V161() V162() V163() set
K19(K20(K20(1,1),REAL)) is set
K20(REAL,REAL) is V161() V162() V163() set
K20(K20(REAL,REAL),REAL) is V161() V162() V163() set
K19(K20(K20(REAL,REAL),REAL)) is set
2 is non empty natural V28() real ext-real positive non negative V123() V124() V171() V172() V173() V174() V175() V176() V211() V213() Element of NAT
K20(2,2) is RAT -valued INT -valued V161() V162() V163() V164() set
K20(K20(2,2),REAL) is V161() V162() V163() set
K19(K20(K20(2,2),REAL)) is set
RealSpace is strict V122() MetrStruct
R^1 is non empty strict TopSpace-like V122() TopStruct
K19(K20(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V137() V183() V184() V185() V186() V187() V188() V189() strict RLTopStruct
the carrier of (TOP-REAL 2) is functional non empty set
K19( the carrier of (TOP-REAL 2)) is set
K20( the carrier of (TOP-REAL 2),REAL) is V161() V162() V163() set
K19(K20( the carrier of (TOP-REAL 2),REAL)) is set
NonZero (TOP-REAL 2) is functional Element of K19( the carrier of (TOP-REAL 2))
[#] (TOP-REAL 2) is functional non empty non proper open closed dense non boundary Element of K19( the carrier of (TOP-REAL 2))
0. (TOP-REAL 2) is Relation-like Function-like V43(2) FinSequence-like V55( TOP-REAL 2) V161() V162() V163() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of 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))
K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))) is set
K19(K20((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)))) 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
K20(COMPLEX,COMPLEX) is V161() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(COMPLEX,REAL) is V161() V162() V163() set
K19(K20(COMPLEX,REAL)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V161() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(RAT,RAT) is RAT -valued V161() V162() V163() set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is RAT -valued V161() V162() V163() set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is RAT -valued INT -valued V161() V162() V163() set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is RAT -valued INT -valued V161() V162() V163() set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is RAT -valued INT -valued V161() V162() V163() V164() set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued V161() V162() V163() V164() set
K19(K20(K20(NAT,NAT),NAT)) is set
{} is Function-like functional empty V171() V172() V173() V174() V175() V176() V177() V213() V216() set
the Function-like functional empty V171() V172() V173() V174() V175() V176() V177() V213() V216() set is Function-like functional empty V171() V172() V173() V174() V175() V176() V177() V213() V216() set
the carrier of R^1 is non empty V171() V172() V173() set
K19( the carrier of R^1) is set
0 is Function-like functional empty natural V28() real ext-real non positive non negative V123() V124() V171() V172() V173() V174() V175() V176() V177() V213() V216() Element of NAT
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V122() SubSpace of R^1
- 1 is V28() real ext-real non positive Element of REAL
|[0,0]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
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 V18( the carrier of (TOP-REAL 2), REAL ) V161() V162() V163() 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 V18( the carrier of (TOP-REAL 2), REAL ) V161() V162() V163() continuous Element of K19(K20( the carrier of (TOP-REAL 2),REAL))
(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,1.] is V171() V172() V173() V216() Element of K19(REAL)
R^2-unit_square is functional non empty closed compact being_simple_closed_curve Element of K19( the carrier of (TOP-REAL 2))
|[0,1]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,0]|,|[0,1]|) is functional non empty closed compact V237( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[0,0]|) + (b1 * |[0,1]|)) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
|[1,1]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,1]|,|[1,1]|) is functional non empty closed compact V237( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[0,1]|) + (b1 * |[1,1]|)) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is functional non empty closed Element of K19( the carrier of (TOP-REAL 2))
|[1,0]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
LSeg (|[1,1]|,|[1,0]|) is functional non empty closed compact V237( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[1,1]|) + (b1 * |[1,0]|)) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (|[1,0]|,|[0,0]|) is functional non empty closed compact V237( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[1,0]|) + (b1 * |[0,0]|)) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)) is functional non empty closed Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is functional non empty closed Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = 0 & b1 `2 <= 1 & 0 <= b1 `2 ) or ( b1 `1 <= 1 & 0 <= b1 `1 & b1 `2 = 1 ) or ( b1 `1 <= 1 & 0 <= b1 `1 & b1 `2 = 0 ) or ( b1 `1 = 1 & b1 `2 <= 1 & 0 <= b1 `2 ) ) } is set
Sq_Circ is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like one-to-one non empty total V18( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : ( ( - 1 = b1 `1 & - 1 <= b1 `2 & b1 `2 <= 1 ) or ( b1 `1 = 1 & - 1 <= b1 `2 & b1 `2 <= 1 ) or ( - 1 = b1 `2 & - 1 <= b1 `1 & b1 `1 <= 1 ) or ( 1 = b1 `2 & - 1 <= b1 `1 & b1 `1 <= 1 ) ) } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : |.b1.| = 1 } is set
Sq_Circ " is Relation-like Function-like one-to-one set
rng Sq_Circ is functional Element of K19( the carrier of (TOP-REAL 2))
I[01] is non empty strict TopSpace-like V122() SubSpace of R^1
the carrier of I[01] is non empty V171() V172() V173() set
K20( the carrier of I[01], the carrier of (TOP-REAL 2)) is set
K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2))) is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : |.b1.| <= 1 } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : ( |.b1.| = 1 & b1 `2 <= b1 `1 & - (b1 `1) <= b1 `2 ) } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : ( |.b1.| = 1 & b1 `1 <= b1 `2 & b1 `2 <= - (b1 `1) ) } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : ( |.b1.| = 1 & b1 `1 <= b1 `2 & - (b1 `1) <= b1 `2 ) } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : ( |.b1.| = 1 & b1 `2 <= b1 `1 & b1 `2 <= - (b1 `1) ) } is set
|[(- 1),0]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|[0,(- 1)]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | R^2-unit_square is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | R^2-unit_square) is non empty set
3 is non empty natural V28() real ext-real positive non negative V123() V124() V171() V172() V173() V174() V175() V176() V211() V213() Element of NAT
K19( the carrier of I[01]) is set
1 / 2 is V28() real ext-real non negative Element of REAL
p2 is V28() real ext-real set
p1 is V28() real ext-real set
p2 ^2 is V28() real ext-real set
p2 * p2 is V28() real ext-real set
1 + (p2 ^2) is V28() real ext-real Element of REAL
sqrt (1 + (p2 ^2)) is V28() real ext-real Element of REAL
p1 * (sqrt (1 + (p2 ^2))) is V28() real ext-real Element of REAL
p1 ^2 is V28() real ext-real set
p1 * p1 is V28() real ext-real set
1 + (p1 ^2) is V28() real ext-real Element of REAL
sqrt (1 + (p1 ^2)) is V28() real ext-real Element of REAL
p2 * (sqrt (1 + (p1 ^2))) is V28() real ext-real Element of REAL
- p2 is V28() real ext-real set
(- p2) * (sqrt (1 + (p1 ^2))) is V28() real ext-real Element of REAL
(- p2) ^2 is V28() real ext-real set
(- p2) * (- p2) is V28() real ext-real set
((- p2) ^2) * (1 + (p1 ^2)) is V28() real ext-real Element of REAL
sqrt (((- p2) ^2) * (1 + (p1 ^2))) is V28() real ext-real Element of REAL
- p1 is V28() real ext-real set
(- p1) * (sqrt (1 + (p2 ^2))) is V28() real ext-real Element of REAL
(- p1) ^2 is V28() real ext-real set
(- p1) * (- p1) is V28() real ext-real set
((- p1) ^2) * (1 + (p2 ^2)) is V28() real ext-real Element of REAL
sqrt (((- p1) ^2) * (1 + (p2 ^2))) is V28() real ext-real Element of REAL
(p2 ^2) * 1 is V28() real ext-real Element of REAL
(p2 ^2) * (p1 ^2) is V28() real ext-real set
((p2 ^2) * 1) + ((p2 ^2) * (p1 ^2)) is V28() real ext-real Element of REAL
(p1 ^2) * 1 is V28() real ext-real Element of REAL
(p1 ^2) * (p2 ^2) is V28() real ext-real set
((p1 ^2) * 1) + ((p1 ^2) * (p2 ^2)) is V28() real ext-real Element of REAL
- (p2 * (sqrt (1 + (p1 ^2)))) is V28() real ext-real Element of REAL
- (p1 * (sqrt (1 + (p2 ^2)))) is V28() real ext-real Element of REAL
p1 is V28() real ext-real set
p2 is V28() real ext-real set
p2 ^2 is V28() real ext-real set
p2 * p2 is V28() real ext-real set
1 + (p2 ^2) is V28() real ext-real Element of REAL
sqrt (1 + (p2 ^2)) is V28() real ext-real Element of REAL
p1 * (sqrt (1 + (p2 ^2))) is V28() real ext-real Element of REAL
p1 ^2 is V28() real ext-real set
p1 * p1 is V28() real ext-real set
1 + (p1 ^2) is V28() real ext-real Element of REAL
sqrt (1 + (p1 ^2)) is V28() real ext-real Element of REAL
p2 * (sqrt (1 + (p1 ^2))) is V28() real ext-real Element of REAL
p1 is V28() real ext-real set
p2 is V28() real ext-real set
p1 ^2 is V28() real ext-real set
p1 * p1 is V28() real ext-real set
1 + (p1 ^2) is V28() real ext-real Element of REAL
sqrt (1 + (p1 ^2)) is V28() real ext-real Element of REAL
p2 * (sqrt (1 + (p1 ^2))) is V28() real ext-real Element of REAL
p2 ^2 is V28() real ext-real set
p2 * p2 is V28() real ext-real set
1 + (p2 ^2) is V28() real ext-real Element of REAL
sqrt (1 + (p2 ^2)) is V28() real ext-real Element of REAL
p1 * (sqrt (1 + (p2 ^2))) is V28() real ext-real Element of REAL
- p1 is V28() real ext-real set
- p2 is V28() real ext-real set
(- p2) ^2 is V28() real ext-real set
(- p2) * (- p2) is V28() real ext-real set
1 + ((- p2) ^2) is V28() real ext-real Element of REAL
sqrt (1 + ((- p2) ^2)) is V28() real ext-real Element of REAL
(- p1) * (sqrt (1 + ((- p2) ^2))) is V28() real ext-real Element of REAL
(- p1) ^2 is V28() real ext-real set
(- p1) * (- p1) is V28() real ext-real set
1 + ((- p1) ^2) is V28() real ext-real Element of REAL
sqrt (1 + ((- p1) ^2)) is V28() real ext-real Element of REAL
(- p2) * (sqrt (1 + ((- p1) ^2))) is V28() real ext-real Element of REAL
- (p1 * (sqrt (1 + (p2 ^2)))) is V28() real ext-real Element of REAL
- (p2 * (sqrt (1 + (p1 ^2)))) is V28() real ext-real Element of REAL
p2 is V28() real ext-real set
p3 is V28() real ext-real set
p1 is V28() real ext-real set
|[p1,p2]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|[p1,p3]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
LSeg (|[p1,p2]|,|[p1,p3]|) is functional non empty closed compact V237( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[p1,p2]|) + (b1 * |[p1,p3]|)) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p4 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p4 `1 is V28() real ext-real Element of REAL
p4 `2 is V28() real ext-real Element of REAL
|[p1,p2]| `2 is V28() real ext-real Element of REAL
|[p1,p3]| `2 is V28() real ext-real Element of REAL
p3 is V28() real ext-real set
p2 is V28() real ext-real set
p1 is V28() real ext-real set
|[p1,p2]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|[p1,p3]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
LSeg (|[p1,p2]|,|[p1,p3]|) is functional non empty closed compact V237( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[p1,p2]|) + (b1 * |[p1,p3]|)) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p4 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p4 `1 is V28() real ext-real Element of REAL
p4 `2 is V28() real ext-real Element of REAL
p3 - p2 is V28() real ext-real set
(p4 `2) - p2 is V28() real ext-real Element of REAL
((p4 `2) - p2) / (p3 - p2) is V28() real ext-real Element of REAL
K is V28() real ext-real Element of REAL
1 - K is V28() real ext-real Element of REAL
(1 - K) * |[p1,p2]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
K * |[p1,p3]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
((1 - K) * |[p1,p2]|) + (K * |[p1,p3]|) is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
(1 - K) * p1 is V28() real ext-real Element of REAL
(1 - K) * p2 is V28() real ext-real Element of REAL
|[((1 - K) * p1),((1 - K) * p2)]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|[((1 - K) * p1),((1 - K) * p2)]| + (K * |[p1,p3]|) is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
K * p1 is V28() real ext-real Element of REAL
K * p3 is V28() real ext-real Element of REAL
|[(K * p1),(K * p3)]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|[((1 - K) * p1),((1 - K) * p2)]| + |[(K * p1),(K * p3)]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
((1 - K) * p1) + (K * p1) is V28() real ext-real Element of REAL
((1 - K) * p2) + (K * p3) is V28() real ext-real Element of REAL
|[(((1 - K) * p1) + (K * p1)),(((1 - K) * p2) + (K * p3))]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
K * (p3 - p2) is V28() real ext-real Element of REAL
p2 + (K * (p3 - p2)) is V28() real ext-real Element of REAL
|[p1,(p2 + (K * (p3 - p2)))]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p2 + ((p4 `2) - p2) is V28() real ext-real Element of REAL
|[p1,(p2 + ((p4 `2) - p2))]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
(p3 - p2) / (p3 - p2) is V28() real ext-real Element of COMPLEX
p1 is V28() real ext-real set
p2 is V28() real ext-real set
p3 is V28() real ext-real set
|[p1,p3]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|[p2,p3]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
LSeg (|[p1,p3]|,|[p2,p3]|) is functional non empty closed compact V237( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[p1,p3]|) + (b1 * |[p2,p3]|)) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p4 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p4 `2 is V28() real ext-real Element of REAL
p4 `1 is V28() real ext-real Element of REAL
|[p1,p3]| `1 is V28() real ext-real Element of REAL
|[p2,p3]| `1 is V28() real ext-real Element of REAL
p1 is V28() real ext-real set
p2 is V28() real ext-real set
[.p1,p2.] is V171() V172() V173() V216() Element of K19(REAL)
p3 is V171() V172() V173() Element of K19( the carrier of I[01])
p4 is V171() V172() V173() Element of K19( the carrier of R^1)
K is V171() V172() V173() Element of K19( the carrier of R^1)
R^1 | K is strict TopSpace-like V122() SubSpace of R^1
[#] (R^1 | K) is non proper open closed dense V171() V172() V173() Element of K19( the carrier of (R^1 | K))
the carrier of (R^1 | K) is V171() V172() V173() set
K19( the carrier of (R^1 | K)) is set
p4 /\ ([#] (R^1 | K)) is V171() V172() V173() Element of K19( the carrier of (R^1 | K))
p1 is TopStruct
the carrier of p1 is set
[#] p1 is non proper dense Element of K19( the carrier of p1)
K19( the carrier of p1) is set
p2 is non empty TopStruct
the carrier of p2 is non empty set
K20( the carrier of p1, the carrier of p2) is set
K19(K20( the carrier of p1, the carrier of p2)) is set
p3 is non empty TopStruct
the carrier of p3 is non empty set
K20( the carrier of p1, the carrier of p3) is set
K19(K20( the carrier of p1, the carrier of p3)) is set
p4 is Relation-like the carrier of p1 -defined the carrier of p2 -valued Function-like total V18( the carrier of p1, the carrier of p2) Element of K19(K20( the carrier of p1, the carrier of p2))
dom p4 is Element of K19( the carrier of p1)
K is Relation-like the carrier of p1 -defined the carrier of p3 -valued Function-like total V18( the carrier of p1, the carrier of p3) Element of K19(K20( the carrier of p1, the carrier of p3))
dom K is Element of K19( the carrier of p1)
p1 is non empty TopSpace-like TopStruct
the carrier of p1 is non empty set
K19( the carrier of p1) is set
p2 is non empty Element of K19( the carrier of p1)
p1 | p2 is non empty strict TopSpace-like SubSpace of p1
the carrier of (p1 | p2) is non empty set
K20( the carrier of (p1 | p2), the carrier of p1) is set
K19(K20( the carrier of (p1 | p2), the carrier of p1)) is set
[#] (p1 | p2) is non empty non proper open closed dense non boundary Element of K19( the carrier of (p1 | p2))
K19( the carrier of (p1 | p2)) is set
p3 is Element of the carrier of (p1 | p2)
p4 is Element of the carrier of p1
p3 is Relation-like the carrier of (p1 | p2) -defined the carrier of p1 -valued Function-like non empty total V18( the carrier of (p1 | p2), the carrier of p1) Element of K19(K20( the carrier of (p1 | p2), the carrier of p1))
p3 is Relation-like the carrier of (p1 | p2) -defined the carrier of p1 -valued Function-like non empty total V18( the carrier of (p1 | p2), the carrier of p1) Element of K19(K20( the carrier of (p1 | p2), the carrier of p1))
p4 is Element of the carrier of (p1 | p2)
p3 . p4 is Element of the carrier of p1
p4 is Element of the carrier of (p1 | p2)
p3 . p4 is Element of the carrier of p1
K is Element of K19( the carrier of p1)
K /\ ([#] (p1 | p2)) is Element of K19( the carrier of (p1 | p2))
K0 is Element of K19( the carrier of (p1 | p2))
p3 .: K0 is Element of K19( the carrier of p1)
j is set
dom p3 is Element of K19( the carrier of (p1 | p2))
P is set
p3 . P is set
f is Element of the carrier of (p1 | p2)
p3 . f is Element of the carrier of p1
p4 is Relation-like the carrier of (p1 | p2) -defined the carrier of p1 -valued Function-like non empty total V18( the carrier of (p1 | p2), the carrier of p1) Element of K19(K20( the carrier of (p1 | p2), the carrier of p1))
p1 is non empty TopSpace-like TopStruct
the carrier of p1 is non empty set
K20( the carrier of p1, the carrier of R^1) is V161() V162() V163() set
K19(K20( the carrier of p1, the carrier of R^1)) is set
p2 is Relation-like the carrier of p1 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of p1, the carrier of R^1) V161() V162() V163() Element of K19(K20( the carrier of p1, the carrier of R^1))
p3 is V28() real ext-real set
- p3 is V28() real ext-real set
p4 is Relation-like the carrier of p1 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of p1, the carrier of R^1) V161() V162() V163() Element of K19(K20( the carrier of p1, the carrier of R^1))
K is Element of the carrier of p1
p2 . K is V28() real ext-real Element of the carrier of R^1
p4 . K is V28() real ext-real Element of the carrier of R^1
K0 is V28() real ext-real set
K0 - p3 is V28() real ext-real set
K0 + (- p3) is V28() real ext-real set
p1 is non empty TopSpace-like TopStruct
the carrier of p1 is non empty set
K20( the carrier of p1, the carrier of R^1) is V161() V162() V163() set
K19(K20( the carrier of p1, the carrier of R^1)) is set
p2 is Relation-like the carrier of p1 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of p1, the carrier of R^1) V161() V162() V163() Element of K19(K20( the carrier of p1, the carrier of R^1))
p3 is V28() real ext-real set
p4 is Relation-like the carrier of p1 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of p1, the carrier of R^1) V161() V162() V163() Element of K19(K20( the carrier of p1, the carrier of R^1))
K is Relation-like the carrier of p1 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of p1, the carrier of R^1) V161() V162() V163() Element of K19(K20( the carrier of p1, the carrier of R^1))
K0 is Element of the carrier of p1
p2 . K0 is V28() real ext-real Element of the carrier of R^1
K . K0 is V28() real ext-real Element of the carrier of R^1
j is V28() real ext-real set
p3 - j is V28() real ext-real set
p4 . K0 is V28() real ext-real Element of the carrier of R^1
j - p3 is V28() real ext-real set
- (j - p3) is V28() real ext-real set
p1 is non empty TopSpace-like TopStruct
the carrier of p1 is non empty set
K20( the carrier of p1, the carrier of R^1) is V161() V162() V163() set
K19(K20( the carrier of p1, the carrier of R^1)) is set
p2 is natural V28() real ext-real V123() V124() V171() V172() V173() V174() V175() V176() V213() Element of NAT
TOP-REAL p2 is non empty TopSpace-like T_0 T_1 T_2 V137() V183() V184() V185() V186() V187() V188() V189() strict RLTopStruct
the carrier of (TOP-REAL p2) is functional non empty set
K20( the carrier of p1, the carrier of (TOP-REAL p2)) is set
K19(K20( the carrier of p1, the carrier of (TOP-REAL p2))) is set
p3 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
p4 is Relation-like the carrier of p1 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of p1, the carrier of R^1) V161() V162() V163() Element of K19(K20( the carrier of p1, the carrier of R^1))
K is Element of the carrier of p1
p4 . K is V28() real ext-real set
(p4 . K) * p3 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
K is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
K is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
K19( the carrier of (TOP-REAL p2)) is set
K0 is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
K19( the carrier of p1) is set
j is Element of the carrier of p1
K0 . j is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
P is functional Element of K19( the carrier of (TOP-REAL p2))
Int P is functional open Element of K19( the carrier of (TOP-REAL p2))
Euclid p2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid p2) is non empty set
f is Element of the carrier of (Euclid p2)
g is V28() real ext-real set
Ball (f,g) is Element of K19( the carrier of (Euclid p2))
K19( the carrier of (Euclid p2)) is set
0. (TOP-REAL p2) is Relation-like Function-like V43(p2) FinSequence-like V55( TOP-REAL p2) V161() V162() V163() Element of the carrier of (TOP-REAL p2)
the ZeroF of (TOP-REAL p2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|.p3.| is V28() real ext-real non negative Element of REAL
g / |.p3.| is V28() real ext-real Element of REAL
p4 . j is V28() real ext-real Element of the carrier of R^1
(p4 . j) - (g / |.p3.|) is V28() real ext-real Element of REAL
(p4 . j) + (g / |.p3.|) is V28() real ext-real Element of REAL
].((p4 . j) - (g / |.p3.|)),((p4 . j) + (g / |.p3.|)).[ is V171() V172() V173() V211() V212() V216() Element of K19(REAL)
f1 is V171() V172() V173() Element of K19( the carrier of R^1)
g1 is Element of K19( the carrier of p1)
p4 .: g1 is V171() V172() V173() Element of K19( the carrier of R^1)
K0 .: g1 is functional Element of K19( the carrier of (TOP-REAL p2))
C0 is set
dom K0 is Element of K19( the carrier of p1)
q1 is set
K0 . q1 is Relation-like Function-like set
dom p4 is Element of K19( the carrier of p1)
q2 is Element of the carrier of p1
p4 . q2 is V28() real ext-real Element of the carrier of R^1
(p4 . q2) - (p4 . j) is V28() real ext-real set
abs ((p4 . q2) - (p4 . j)) is V28() real ext-real Element of REAL
q4 is V28() real ext-real Element of REAL
q3 is V28() real ext-real Element of REAL
q4 - q3 is V28() real ext-real Element of REAL
abs (q4 - q3) is V28() real ext-real Element of REAL
q3 - q4 is V28() real ext-real Element of REAL
abs (q3 - q4) is V28() real ext-real Element of REAL
K0 . q2 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(p4 . j) * p3 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(K0 . j) - (K0 . q2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|.((K0 . j) - (K0 . q2)).| is V28() real ext-real non negative Element of REAL
(p4 . q2) * p3 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((p4 . j) * p3) - ((p4 . q2) * p3) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|.(((p4 . j) * p3) - ((p4 . q2) * p3)).| is V28() real ext-real non negative Element of REAL
(p4 . j) - (p4 . q2) is V28() real ext-real set
((p4 . j) - (p4 . q2)) * p3 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|.(((p4 . j) - (p4 . q2)) * p3).| is V28() real ext-real non negative Element of REAL
(abs (q4 - q3)) * |.p3.| is V28() real ext-real Element of REAL
(g / |.p3.|) * |.p3.| is V28() real ext-real Element of REAL
(abs ((p4 . q2) - (p4 . j))) * |.p3.| is V28() real ext-real Element of REAL
y is Element of the carrier of (Euclid p2)
dist (f,y) is V28() real ext-real Element of REAL
0. (TOP-REAL p2) is Relation-like Function-like V43(p2) FinSequence-like V55( TOP-REAL p2) V161() V162() V163() Element of the carrier of (TOP-REAL p2)
the ZeroF of (TOP-REAL p2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
s is Element of the carrier of p1
K0 . s is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
p4 . s is V28() real ext-real Element of the carrier of R^1
(p4 . s) * p3 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
[#] p1 is non empty non proper open closed dense non boundary Element of K19( the carrier of p1)
K0 .: ([#] p1) is functional Element of K19( the carrier of (TOP-REAL p2))
f1 is set
dom K0 is Element of K19( the carrier of p1)
g1 is set
K0 . g1 is Relation-like Function-like set
0. (TOP-REAL p2) is Relation-like Function-like V43(p2) FinSequence-like V55( TOP-REAL p2) V161() V162() V163() Element of the carrier of (TOP-REAL p2)
the ZeroF of (TOP-REAL p2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
0. (TOP-REAL p2) is Relation-like Function-like V43(p2) FinSequence-like V55( TOP-REAL p2) V161() V162() V163() Element of the carrier of (TOP-REAL p2)
the ZeroF of (TOP-REAL p2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
s is Element of K19( the carrier of p1)
K0 .: s is functional Element of K19( the carrier of (TOP-REAL p2))
f1 is Element of K19( the carrier of p1)
K0 .: f1 is functional Element of K19( the carrier of (TOP-REAL p2))
Sq_Circ . |[(- 1),0]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|[(- 1),0]| `1 is V28() real ext-real Element of REAL
|[(- 1),0]| `2 is V28() real ext-real Element of REAL
- (|[(- 1),0]| `1) is V28() real ext-real Element of REAL
(|[(- 1),0]| `2) / (|[(- 1),0]| `1) is V28() real ext-real Element of REAL
((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2 is V28() real ext-real Element of REAL
((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) * ((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) is V28() real ext-real set
1 + (((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2) is V28() real ext-real Element of REAL
sqrt (1 + (((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2)) is V28() real ext-real Element of REAL
(|[(- 1),0]| `1) / (sqrt (1 + (((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2))) is V28() real ext-real Element of REAL
(|[(- 1),0]| `2) / (sqrt (1 + (((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2))) is V28() real ext-real Element of REAL
|[((|[(- 1),0]| `1) / (sqrt (1 + (((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2)))),((|[(- 1),0]| `2) / (sqrt (1 + (((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2))))]| is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p1 is functional non empty closed compact Element of K19( the carrier of (TOP-REAL 2))
W-min p1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p1 is non empty TopSpace-like TopStruct
the carrier of p1 is non empty set
p2 is natural V28() real ext-real V123() V124() V171() V172() V173() V174() V175() V176() V213() Element of NAT
TOP-REAL p2 is non empty TopSpace-like T_0 T_1 T_2 V137() V183() V184() V185() V186() V187() V188() V189() strict RLTopStruct
the carrier of (TOP-REAL p2) is functional non empty set
K20( the carrier of p1, the carrier of (TOP-REAL p2)) is set
K19(K20( the carrier of p1, the carrier of (TOP-REAL p2))) is set
p3 is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
p4 is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
K is Element of the carrier of p1
p3 . K is Relation-like Function-like set
p4 . K is Relation-like Function-like set
p3 . K is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
p4 . K is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(p3 . K) + (p4 . K) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
f is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
g is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
f + g is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
K is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
K is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
K0 is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
j is Element of the carrier of p1
K0 . j is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
p3 . j is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
p4 . j is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(p3 . j) + (p4 . j) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
K19( the carrier of (TOP-REAL p2)) is set
K19( the carrier of p1) is set
j is Element of the carrier of p1
K0 . j is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
P is functional Element of K19( the carrier of (TOP-REAL p2))
Int P is functional open Element of K19( the carrier of (TOP-REAL p2))
Euclid p2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid p2) is non empty set
f is Element of the carrier of (Euclid p2)
g is V28() real ext-real set
Ball (f,g) is Element of K19( the carrier of (Euclid p2))
K19( the carrier of (Euclid p2)) is set
p3 . j is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
s is Element of the carrier of (Euclid p2)
g / 2 is V28() real ext-real Element of REAL
Ball (s,(g / 2)) is Element of K19( the carrier of (Euclid p2))
p4 . j is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
g1 is Element of the carrier of (Euclid p2)
Ball (g1,(g / 2)) is Element of K19( the carrier of (Euclid p2))
f1 is functional Element of K19( the carrier of (TOP-REAL p2))
the topology of (TOP-REAL p2) is non empty open Element of K19(K19( the carrier of (TOP-REAL p2)))
K19(K19( the carrier of (TOP-REAL p2))) is set
TopStruct(# the carrier of (TOP-REAL p2), the topology of (TOP-REAL p2) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid p2) is TopStruct
the carrier of (TopSpaceMetr (Euclid p2)) is set
K19( the carrier of (TopSpaceMetr (Euclid p2))) is set
C0 is functional Element of K19( the carrier of (TOP-REAL p2))
q1 is Element of K19( the carrier of (TopSpaceMetr (Euclid p2)))
q3 is Element of K19( the carrier of p1)
p3 .: q3 is functional Element of K19( the carrier of (TOP-REAL p2))
q2 is Element of K19( the carrier of (TopSpaceMetr (Euclid p2)))
q4 is Element of K19( the carrier of p1)
p4 .: q4 is functional Element of K19( the carrier of (TOP-REAL p2))
q3 /\ q4 is Element of K19( the carrier of p1)
K0 .: (q3 /\ q4) is functional Element of K19( the carrier of (TOP-REAL p2))
x1 is set
dom K0 is Element of K19( the carrier of p1)
x2 is set
K0 . x2 is Relation-like Function-like set
dom p3 is Element of K19( the carrier of p1)
x2 is Element of the carrier of p1
p3 . x2 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
r1 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
r2 is Element of the carrier of (Euclid p2)
dist (s,r2) is V28() real ext-real Element of REAL
(p3 . j) - (p3 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|.((p3 . j) - (p3 . x2)).| is V28() real ext-real non negative Element of REAL
dom p4 is Element of K19( the carrier of p1)
p4 . x2 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
gr1 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
gr2 is Element of the carrier of (Euclid p2)
dist (g1,gr2) is V28() real ext-real Element of REAL
(p4 . j) - (p4 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|.((p4 . j) - (p4 . x2)).| is V28() real ext-real non negative Element of REAL
r1 + gr1 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
K0 . x2 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(p3 . x2) + (p4 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(p3 . j) + (p4 . j) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((p3 . j) + (p4 . j)) - ((p3 . x2) + (p4 . x2)) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((p3 . j) + (p4 . j)) - (p3 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(((p3 . j) + (p4 . j)) - (p3 . x2)) - (p4 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
- (p3 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((p3 . j) + (p4 . j)) + (- (p3 . x2)) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(((p3 . j) + (p4 . j)) + (- (p3 . x2))) - (p4 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
- (p4 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(((p3 . j) + (p4 . j)) + (- (p3 . x2))) + (- (p4 . x2)) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(p3 . j) + (- (p3 . x2)) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((p3 . j) + (- (p3 . x2))) + (p4 . j) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(((p3 . j) + (- (p3 . x2))) + (p4 . j)) + (- (p4 . x2)) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(p4 . j) + (- (p4 . x2)) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((p3 . j) + (- (p3 . x2))) + ((p4 . j) + (- (p4 . x2))) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((p3 . j) - (p3 . x2)) + ((p4 . j) + (- (p4 . x2))) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((p3 . j) - (p3 . x2)) + ((p4 . j) - (p4 . x2)) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|.(((p3 . j) + (p4 . j)) - ((p3 . x2) + (p4 . x2))).| is V28() real ext-real non negative Element of REAL
|.((p3 . j) - (p3 . x2)).| + |.((p4 . j) - (p4 . x2)).| is V28() real ext-real non negative Element of REAL
(g / 2) + (g / 2) is V28() real ext-real Element of REAL
(K0 . j) - (K0 . x2) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|.((K0 . j) - (K0 . x2)).| is V28() real ext-real non negative Element of REAL
bb0 is Element of the carrier of (Euclid p2)
dist (f,bb0) is V28() real ext-real Element of REAL
p1 is non empty TopSpace-like TopStruct
the carrier of p1 is non empty set
K20( the carrier of p1, the carrier of R^1) is V161() V162() V163() set
K19(K20( the carrier of p1, the carrier of R^1)) is set
p2 is natural V28() real ext-real V123() V124() V171() V172() V173() V174() V175() V176() V213() Element of NAT
TOP-REAL p2 is non empty TopSpace-like T_0 T_1 T_2 V137() V183() V184() V185() V186() V187() V188() V189() strict RLTopStruct
the carrier of (TOP-REAL p2) is functional non empty set
K20( the carrier of p1, the carrier of (TOP-REAL p2)) is set
K19(K20( the carrier of p1, the carrier of (TOP-REAL p2))) is set
p3 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
p4 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
K is Relation-like the carrier of p1 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of p1, the carrier of R^1) V161() V162() V163() Element of K19(K20( the carrier of p1, the carrier of R^1))
K0 is Relation-like the carrier of p1 -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of p1, the carrier of R^1) V161() V162() V163() Element of K19(K20( the carrier of p1, the carrier of R^1))
j is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
P is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
f is Relation-like the carrier of p1 -defined the carrier of (TOP-REAL p2) -valued Function-like non empty total V18( the carrier of p1, the carrier of (TOP-REAL p2)) Element of K19(K20( the carrier of p1, the carrier of (TOP-REAL p2)))
g is Element of the carrier of p1
f . g is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
K . g is V28() real ext-real Element of the carrier of R^1
(K . g) * p3 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
K0 . g is V28() real ext-real Element of the carrier of R^1
(K0 . g) * p4 is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
((K . g) * p3) + ((K0 . g) * p4) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
j . g is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
P . g is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(j . g) + (P . g) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
(j . g) + ((K0 . g) * p4) is Relation-like Function-like V43(p2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL p2)
|[(- 1),0]| `1 is V28() real ext-real Element of REAL
|[(- 1),0]| `2 is V28() real ext-real Element of REAL
|[1,0]| `1 is V28() real ext-real Element of REAL
|[1,0]| `2 is V28() real ext-real Element of REAL
|[0,(- 1)]| `1 is V28() real ext-real Element of REAL
|[0,(- 1)]| `2 is V28() real ext-real Element of REAL
|[0,1]| `1 is V28() real ext-real Element of REAL
|[0,1]| `2 is V28() real ext-real Element of REAL
|.|[(- 1),0]|.| is V28() real ext-real non negative Element of REAL
(- 1) ^2 is V28() real ext-real Element of REAL
(- 1) * (- 1) is V28() real ext-real non negative set
0 ^2 is V28() real ext-real Element of REAL
0 * 0 is Function-like functional empty V28() real ext-real non positive non negative V171() V172() V173() V174() V175() V176() V177() V213() V216() set
((- 1) ^2) + (0 ^2) is V28() real ext-real Element of REAL
sqrt (((- 1) ^2) + (0 ^2)) is V28() real ext-real Element of REAL
|.|[1,0]|.| is V28() real ext-real non negative Element of REAL
1 ^2 is V28() real ext-real Element of REAL
1 * 1 is V28() real ext-real non negative set
(1 ^2) + (0 ^2) is V28() real ext-real Element of REAL
sqrt ((1 ^2) + (0 ^2)) is V28() real ext-real Element of REAL
|.|[0,(- 1)]|.| is V28() real ext-real non negative Element of REAL
(0 ^2) + ((- 1) ^2) is V28() real ext-real Element of REAL
sqrt ((0 ^2) + ((- 1) ^2)) is V28() real ext-real Element of REAL
|.|[0,1]|.| is V28() real ext-real non negative Element of REAL
(0 ^2) + (1 ^2) is V28() real ext-real Element of REAL
sqrt ((0 ^2) + (1 ^2)) is V28() real ext-real Element of REAL
p1 is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
p2 is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng p1 is functional Element of K19( the carrier of (TOP-REAL 2))
rng p2 is functional Element of K19( the carrier of (TOP-REAL 2))
p3 is functional Element of K19( the carrier of (TOP-REAL 2))
p4 is functional Element of K19( the carrier of (TOP-REAL 2))
K is functional Element of K19( the carrier of (TOP-REAL 2))
K0 is functional Element of K19( the carrier of (TOP-REAL 2))
j is functional Element of K19( the carrier of (TOP-REAL 2))
P is V28() real ext-real Element of the carrier of I[01]
f is V28() real ext-real Element of the carrier of I[01]
p1 . P is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p1 . f is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p2 . P is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p2 . f is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p1 . 1 is Relation-like Function-like set
p1 . 0 is Relation-like Function-like set
g is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
g . 0 is Relation-like Function-like set
g . 1 is Relation-like Function-like set
rng g is functional Element of K19( the carrier of (TOP-REAL 2))
p1 is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
p2 is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng p1 is functional Element of K19( the carrier of (TOP-REAL 2))
rng p2 is functional Element of K19( the carrier of (TOP-REAL 2))
p3 is functional Element of K19( the carrier of (TOP-REAL 2))
p4 is functional Element of K19( the carrier of (TOP-REAL 2))
K is functional Element of K19( the carrier of (TOP-REAL 2))
K0 is functional Element of K19( the carrier of (TOP-REAL 2))
j is functional Element of K19( the carrier of (TOP-REAL 2))
P is V28() real ext-real Element of the carrier of I[01]
f is V28() real ext-real Element of the carrier of I[01]
p1 . P is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p1 . f is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p2 . P is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p2 . f is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p2 . 1 is Relation-like Function-like set
p2 . 0 is Relation-like Function-like set
g is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
g . 0 is Relation-like Function-like set
g . 1 is Relation-like Function-like set
rng g is functional Element of K19( the carrier of (TOP-REAL 2))
p1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
K is functional non empty closed compact Element of K19( the carrier of (TOP-REAL 2))
K0 is functional Element of K19( the carrier of (TOP-REAL 2))
j is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
P is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
j . 0 is Relation-like Function-like set
j . 1 is Relation-like Function-like set
P . 0 is Relation-like Function-like set
P . 1 is Relation-like Function-like set
rng j is functional Element of K19( the carrier of (TOP-REAL 2))
rng P is functional Element of K19( the carrier of (TOP-REAL 2))
dom j is V171() V172() V173() Element of K19( the carrier of I[01])
dom P is V171() V172() V173() Element of K19( the carrier of I[01])
f is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
f . p1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . p2 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . p3 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . p4 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f * j is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
f * P is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
g is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
dom g is V171() V172() V173() Element of K19( the carrier of I[01])
s is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
dom s is V171() V172() V173() Element of K19( the carrier of I[01])
g . 1 is Relation-like Function-like set
s . 1 is Relation-like Function-like set
g . 0 is Relation-like Function-like set
s . 0 is Relation-like Function-like set
rng g is functional Element of K19( the carrier of (TOP-REAL 2))
f1 is set
g1 is set
g . g1 is Relation-like Function-like set
j . g1 is Relation-like Function-like set
f . (j . g1) is Relation-like Function-like set
C0 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . C0 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|.(f . C0).| is V28() real ext-real non negative Element of REAL
|.C0.| is V28() real ext-real non negative Element of REAL
q1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|.q1.| is V28() real ext-real non negative Element of REAL
rng s is functional Element of K19( the carrier of (TOP-REAL 2))
f1 is set
g1 is set
s . g1 is Relation-like Function-like set
P . g1 is Relation-like Function-like set
f . (P . g1) is Relation-like Function-like set
C0 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . C0 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|.(f . C0).| is V28() real ext-real non negative Element of REAL
|.C0.| is V28() real ext-real non negative Element of REAL
q1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|.q1.| is V28() real ext-real non negative Element of REAL
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : S3[b1] } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : S4[b1] } is set
- (|[(- 1),0]| `1) is V28() real ext-real Element of REAL
q3 is V28() real ext-real Element of the carrier of I[01]
g . q3 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
g1 is functional Element of K19( the carrier of (TOP-REAL 2))
q2 is V28() real ext-real Element of the carrier of I[01]
g . q2 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f1 is functional Element of K19( the carrier of (TOP-REAL 2))
- (|[0,(- 1)]| `1) is V28() real ext-real Element of REAL
s . q3 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K19( the carrier of (TOP-REAL 2))
- (|[0,1]| `1) is V28() real ext-real Element of REAL
s . q2 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
C0 is functional Element of K19( the carrier of (TOP-REAL 2))
q4 is set
y is set
g . y is Relation-like Function-like set
x1 is set
s . x1 is Relation-like Function-like set
dom f is functional Element of K19( the carrier of (TOP-REAL 2))
P . x1 is Relation-like Function-like set
j . y is Relation-like Function-like set
x2 is Relation-like Function-like set
x2 " is Relation-like Function-like set
(x2 ") . q4 is set
f . (j . y) is Relation-like Function-like set
(x2 ") . (f . (j . y)) is set
f . (P . x1) is Relation-like Function-like set
(x2 ") . (f . (P . x1)) is set
p1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
K is functional non empty closed compact Element of K19( the carrier of (TOP-REAL 2))
K0 is functional Element of K19( the carrier of (TOP-REAL 2))
j is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
P is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
j . 0 is Relation-like Function-like set
j . 1 is Relation-like Function-like set
P . 0 is Relation-like Function-like set
P . 1 is Relation-like Function-like set
rng j is functional Element of K19( the carrier of (TOP-REAL 2))
rng P is functional Element of K19( the carrier of (TOP-REAL 2))
dom j is V171() V172() V173() Element of K19( the carrier of I[01])
dom P is V171() V172() V173() Element of K19( the carrier of I[01])
f is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
f . p1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . p2 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . p3 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . p4 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f * j is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
f * P is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
g is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
dom g is V171() V172() V173() Element of K19( the carrier of I[01])
s is Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total V18( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K19(K20( the carrier of I[01], the carrier of (TOP-REAL 2)))
dom s is V171() V172() V173() Element of K19( the carrier of I[01])
g . 1 is Relation-like Function-like set
s . 1 is Relation-like Function-like set
g . 0 is Relation-like Function-like set
s . 0 is Relation-like Function-like set
rng g is functional Element of K19( the carrier of (TOP-REAL 2))
f1 is set
g1 is set
g . g1 is Relation-like Function-like set
j . g1 is Relation-like Function-like set
f . (j . g1) is Relation-like Function-like set
C0 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . C0 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|.(f . C0).| is V28() real ext-real non negative Element of REAL
|.C0.| is V28() real ext-real non negative Element of REAL
q1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|.q1.| is V28() real ext-real non negative Element of REAL
rng s is functional Element of K19( the carrier of (TOP-REAL 2))
f1 is set
g1 is set
s . g1 is Relation-like Function-like set
P . g1 is Relation-like Function-like set
f . (P . g1) is Relation-like Function-like set
C0 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f . C0 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|.(f . C0).| is V28() real ext-real non negative Element of REAL
|.C0.| is V28() real ext-real non negative Element of REAL
q1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
|.q1.| is V28() real ext-real non negative Element of REAL
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : S3[b1] } is set
{ b1 where b1 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2) : S4[b1] } is set
- (|[(- 1),0]| `1) is V28() real ext-real Element of REAL
q3 is V28() real ext-real Element of the carrier of I[01]
g . q3 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
g1 is functional Element of K19( the carrier of (TOP-REAL 2))
q2 is V28() real ext-real Element of the carrier of I[01]
g . q2 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
f1 is functional Element of K19( the carrier of (TOP-REAL 2))
- (|[0,(- 1)]| `1) is V28() real ext-real Element of REAL
s . q3 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
C0 is functional Element of K19( the carrier of (TOP-REAL 2))
- (|[0,1]| `1) is V28() real ext-real Element of REAL
s . q2 is Relation-like Function-like V43(2) FinSequence-like V161() V162() V163() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K19( the carrier of (TOP-REAL 2))
q4 is set
y is set
g . y is Relation-like Function-like set
x1 is set
s . x1 is Relation-like Function-like set
dom f is functional Element of K19( the carrier of (TOP-REAL 2))
P . x1 is Relation-like Function-like set
j . y is Relation-like Function-like set
x2 is Relation-like Function-like set
x2 " is Relation-like Function-like