:: JGRAPH_6 semantic presentation

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 - b

|[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 - b

(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 - b

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 - b

(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))

{ b

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)))

{ b

{ b

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

{ b

{ b

{ b

{ b

{ b

|[(- 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 - b

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 - b

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 - b

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

{ b

{ b

{ b

{ b

- (|[(- 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

{ b

{ b

{ b

{ b

- (|[(- 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