:: JGRAPH_3 semantic presentation

REAL is non empty V36() V162() V163() V164() V168() set

NAT is V162() V163() V164() V165() V166() V167() V168() Element of K19(REAL)

K19(REAL) is set

COMPLEX is non empty V36() V162() V168() set

omega is V162() V163() V164() V165() V166() V167() V168() set

K19(omega) is set

K232() is non empty strict TopSpace-like V110() TopStruct

the carrier of K232() is non empty V162() V163() V164() set

1 is non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT

K20(1,1) is set

K19(K20(1,1)) is set

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

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

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

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

K20(REAL,REAL) is set

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

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

2 is non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT

K20(2,2) is set

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

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

RealSpace is strict V110() MetrStruct

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

K19(NAT) is set

RAT is non empty V36() V162() V163() V164() V165() V168() set

INT is non empty V36() V162() V163() V164() V165() V166() V168() set

K19(K20(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V128() V174() V175() V176() V177() V178() V179() V180() V186() L15()

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 set

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

{} is Function-like functional empty V162() V163() V164() V165() V166() V167() V168() set

the Function-like functional empty V162() V163() V164() V165() V166() V167() V168() set is Function-like functional empty V162() V163() V164() V165() V166() V167() V168() set

the carrier of R^1 is non empty V162() V163() V164() set

K19( the carrier of R^1) is set

0 is Function-like functional empty natural V28() real ext-real non positive non negative V114() V115() V162() V163() V164() V165() V166() V167() V168() Element of NAT

0. (TOP-REAL 2) is Relation-like Function-like V43(2) V52( TOP-REAL 2) V111() V154() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

|[0,0]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

I[01] is non empty strict TopSpace-like V110() SubSpace of R^1

the carrier of I[01] is non empty V162() V163() V164() 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

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

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

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

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

proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like non empty total quasi_total 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

1.REAL 2 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

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

{ b

{ b

{ b

{ b

{ b

{ b

R^2-unit_square is functional non empty compact being_simple_closed_curve Element of K19( the carrier of (TOP-REAL 2))

{ b

(TOP-REAL 2) | R^2-unit_square is non empty strict TopSpace-like compact 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 V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT

f is V28() real ext-real set

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

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

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

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

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

f is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

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

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

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

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

g is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

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

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

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

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

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

f is Relation-like Function-like set

g is set

f | g is Relation-like Function-like set

C0 is set

(f | g) .: C0 is set

C0 /\ g is set

f .: (C0 /\ g) is set

KXP is set

dom (f | g) is set

KXN is set

(f | g) . KXN is set

f . KXN is set

dom f is set

(dom f) /\ g is set

KXP is set

dom f is set

KXN is set

f . KXN is set

(dom f) /\ g is set

dom (f | g) is set

(f | g) . KXN is set

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

K19( the carrier of f) is set

g is non empty TopSpace-like TopStruct

the carrier of g is non empty set

K19( the carrier of g) is set

K20( the carrier of f, the carrier of g) is set

K19(K20( the carrier of f, the carrier of g)) is set

C0 is Element of the carrier of f

{C0} is non empty compact Element of K19( the carrier of f)

KXP is non empty Element of K19( the carrier of f)

KXP ` is Element of K19( the carrier of f)

f | KXP is non empty strict TopSpace-like SubSpace of f

the carrier of (f | KXP) is non empty set

KXN is non empty Element of K19( the carrier of g)

KXN ` is Element of K19( the carrier of g)

g | KXN is non empty strict TopSpace-like SubSpace of g

the carrier of (g | KXN) is non empty set

K20( the carrier of (f | KXP), the carrier of (g | KXN)) is set

K19(K20( the carrier of (f | KXP), the carrier of (g | KXN))) is set

KYP is Relation-like the carrier of f -defined the carrier of g -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of g))

KYP . C0 is Element of the carrier of g

{(KYP . C0)} is non empty compact Element of K19( the carrier of g)

KYP | KXP is Relation-like the carrier of f -defined the carrier of g -valued Function-like Element of K19(K20( the carrier of f, the carrier of g))

KYN is Element of the carrier of f

KYP . KYN is Element of the carrier of g

O is Element of K19( the carrier of g)

the carrier of f \ (KXP `) is Element of K19( the carrier of f)

(KXP `) ` is Element of K19( the carrier of f)

I is Element of K19( the carrier of g)

p1 is Element of K19( the carrier of g)

[#] (f | KXP) is non empty non proper closed Element of K19( the carrier of (f | KXP))

K19( the carrier of (f | KXP)) is set

ff is Relation-like the carrier of (f | KXP) -defined the carrier of (g | KXN) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (f | KXP), the carrier of (g | KXN)))

ff . KYN is set

[#] (g | KXN) is non empty non proper closed Element of K19( the carrier of (g | KXN))

K19( the carrier of (g | KXN)) is set

I /\ O is Element of K19( the carrier of g)

(I /\ O) /\ KXN is Element of K19( the carrier of g)

y is Element of K19( the carrier of (g | KXN))

the carrier of g \ KXN is Element of K19( the carrier of g)

gg is Element of the carrier of (f | KXP)

ff . gg is Element of the carrier of (g | KXN)

x1 is Element of K19( the carrier of (f | KXP))

ff .: x1 is Element of K19( the carrier of (g | KXN))

x2 is Element of K19( the carrier of f)

x2 /\ ([#] (f | KXP)) is Element of K19( the carrier of (f | KXP))

px is Element of K19( the carrier of f)

q is Element of K19( the carrier of f)

px /\ x2 is Element of K19( the carrier of f)

pu is Element of K19( the carrier of f)

KYP .: pu is Element of K19( the carrier of g)

p4 is set

dom KYP is Element of K19( the carrier of f)

p2 is set

KYP . p2 is set

px ` is Element of K19( the carrier of f)

dom ff is Element of K19( the carrier of (f | KXP))

(dom KYP) /\ KXP is Element of K19( the carrier of f)

ff . p2 is set

g is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

(KXP `2) / (KXP `1) is V28() real ext-real Element of REAL

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

((KXP `2) / (KXP `1)) * ((KXP `2) / (KXP `1)) is V28() real ext-real set

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

sqrt (1 + (((KXP `2) / (KXP `1)) ^2)) is V28() real ext-real Element of REAL

(KXP `1) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))) is V28() real ext-real Element of REAL

(KXP `2) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))) is V28() real ext-real Element of REAL

|[((KXP `1) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2)))),((KXP `2) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(KXP `1) / (KXP `2) is V28() real ext-real Element of REAL

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

((KXP `1) / (KXP `2)) * ((KXP `1) / (KXP `2)) is V28() real ext-real set

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

sqrt (1 + (((KXP `1) / (KXP `2)) ^2)) is V28() real ext-real Element of REAL

(KXP `1) / (sqrt (1 + (((KXP `1) / (KXP `2)) ^2))) is V28() real ext-real Element of REAL

(KXP `2) / (sqrt (1 + (((KXP `1) / (KXP `2)) ^2))) is V28() real ext-real Element of REAL

|[((KXP `1) / (sqrt (1 + (((KXP `1) / (KXP `2)) ^2)))),((KXP `2) / (sqrt (1 + (((KXP `1) / (KXP `2)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

(g `2) / (g `1) is V28() real ext-real Element of REAL

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

((g `2) / (g `1)) * ((g `2) / (g `1)) is V28() real ext-real set

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

sqrt (1 + (((g `2) / (g `1)) ^2)) is V28() real ext-real Element of REAL

(g `1) / (sqrt (1 + (((g `2) / (g `1)) ^2))) is V28() real ext-real Element of REAL

(g `2) / (sqrt (1 + (((g `2) / (g `1)) ^2))) is V28() real ext-real Element of REAL

|[((g `1) / (sqrt (1 + (((g `2) / (g `1)) ^2)))),((g `2) / (sqrt (1 + (((g `2) / (g `1)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

KXN is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

(KXN `2) / (KXN `1) is V28() real ext-real Element of REAL

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

((KXN `2) / (KXN `1)) * ((KXN `2) / (KXN `1)) is V28() real ext-real set

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

sqrt (1 + (((KXN `2) / (KXN `1)) ^2)) is V28() real ext-real Element of REAL

(KXN `1) / (sqrt (1 + (((KXN `2) / (KXN `1)) ^2))) is V28() real ext-real Element of REAL

(KXN `2) / (sqrt (1 + (((KXN `2) / (KXN `1)) ^2))) is V28() real ext-real Element of REAL

|[((KXN `1) / (sqrt (1 + (((KXN `2) / (KXN `1)) ^2)))),((KXN `2) / (sqrt (1 + (((KXN `2) / (KXN `1)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(KXN `1) / (KXN `2) is V28() real ext-real Element of REAL

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

((KXN `1) / (KXN `2)) * ((KXN `1) / (KXN `2)) is V28() real ext-real set

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

sqrt (1 + (((KXN `1) / (KXN `2)) ^2)) is V28() real ext-real Element of REAL

(KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) is V28() real ext-real Element of REAL

(KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) is V28() real ext-real Element of REAL

|[((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))),((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

(g `1) / (g `2) is V28() real ext-real Element of REAL

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

((g `1) / (g `2)) * ((g `1) / (g `2)) is V28() real ext-real set

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

sqrt (1 + (((g `1) / (g `2)) ^2)) is V28() real ext-real Element of REAL

(g `1) / (sqrt (1 + (((g `1) / (g `2)) ^2))) is V28() real ext-real Element of REAL

(g `2) / (sqrt (1 + (((g `1) / (g `2)) ^2))) is V28() real ext-real Element of REAL

|[((g `1) / (sqrt (1 + (((g `1) / (g `2)) ^2)))),((g `2) / (sqrt (1 + (((g `1) / (g `2)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

KXN is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

(KXN `2) / (KXN `1) is V28() real ext-real Element of REAL

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

((KXN `2) / (KXN `1)) * ((KXN `2) / (KXN `1)) is V28() real ext-real set

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

sqrt (1 + (((KXN `2) / (KXN `1)) ^2)) is V28() real ext-real Element of REAL

(KXN `1) / (sqrt (1 + (((KXN `2) / (KXN `1)) ^2))) is V28() real ext-real Element of REAL

(KXN `2) / (sqrt (1 + (((KXN `2) / (KXN `1)) ^2))) is V28() real ext-real Element of REAL

|[((KXN `1) / (sqrt (1 + (((KXN `2) / (KXN `1)) ^2)))),((KXN `2) / (sqrt (1 + (((KXN `2) / (KXN `1)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(KXN `1) / (KXN `2) is V28() real ext-real Element of REAL

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

((KXN `1) / (KXN `2)) * ((KXN `1) / (KXN `2)) is V28() real ext-real set

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

sqrt (1 + (((KXN `1) / (KXN `2)) ^2)) is V28() real ext-real Element of REAL

(KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) is V28() real ext-real Element of REAL

(KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) is V28() real ext-real Element of REAL

|[((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))),((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

C0 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

g . C0 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

g . KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(KXP `2) / (KXP `1) is V28() real ext-real Element of REAL

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

((KXP `2) / (KXP `1)) * ((KXP `2) / (KXP `1)) is V28() real ext-real set

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

sqrt (1 + (((KXP `2) / (KXP `1)) ^2)) is V28() real ext-real Element of REAL

(KXP `1) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))) is V28() real ext-real Element of REAL

(KXP `2) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))) is V28() real ext-real Element of REAL

|[((KXP `1) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2)))),((KXP `2) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

KXN is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

g . KXN is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(KXN `1) / (KXN `2) is V28() real ext-real Element of REAL

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

((KXN `1) / (KXN `2)) * ((KXN `1) / (KXN `2)) is V28() real ext-real set

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

sqrt (1 + (((KXN `1) / (KXN `2)) ^2)) is V28() real ext-real Element of REAL

(KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) is V28() real ext-real Element of REAL

(KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) is V28() real ext-real Element of REAL

|[((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))),((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

C0 is set

f . C0 is Relation-like Function-like set

g . C0 is Relation-like Function-like set

KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

f . KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

f . KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(KXP `2) / (KXP `1) is V28() real ext-real Element of REAL

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

((KXP `2) / (KXP `1)) * ((KXP `2) / (KXP `1)) is V28() real ext-real set

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

sqrt (1 + (((KXP `2) / (KXP `1)) ^2)) is V28() real ext-real Element of REAL

(KXP `1) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))) is V28() real ext-real Element of REAL

(KXP `2) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))) is V28() real ext-real Element of REAL

|[((KXP `1) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2)))),((KXP `2) / (sqrt (1 + (((KXP `2) / (KXP `1)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

f . KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(KXP `1) / (KXP `2) is V28() real ext-real Element of REAL

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

((KXP `1) / (KXP `2)) * ((KXP `1) / (KXP `2)) is V28() real ext-real set

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

sqrt (1 + (((KXP `1) / (KXP `2)) ^2)) is V28() real ext-real Element of REAL

(KXP `1) / (sqrt (1 + (((KXP `1) / (KXP `2)) ^2))) is V28() real ext-real Element of REAL

(KXP `2) / (sqrt (1 + (((KXP `1) / (KXP `2)) ^2))) is V28() real ext-real Element of REAL

|[((KXP `1) / (sqrt (1 + (((KXP `1) / (KXP `2)) ^2)))),((KXP `2) / (sqrt (1 + (((KXP `1) / (KXP `2)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

KXP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

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

f is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

() . f is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(f `1) / (f `2) is V28() real ext-real Element of REAL

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

((f `1) / (f `2)) * ((f `1) / (f `2)) is V28() real ext-real set

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

sqrt (1 + (((f `1) / (f `2)) ^2)) is V28() real ext-real Element of REAL

(f `1) / (sqrt (1 + (((f `1) / (f `2)) ^2))) is V28() real ext-real Element of REAL

(f `2) / (sqrt (1 + (((f `1) / (f `2)) ^2))) is V28() real ext-real Element of REAL

|[((f `1) / (sqrt (1 + (((f `1) / (f `2)) ^2)))),((f `2) / (sqrt (1 + (((f `1) / (f `2)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

(f `2) / (f `1) is V28() real ext-real Element of REAL

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

((f `2) / (f `1)) * ((f `2) / (f `1)) is V28() real ext-real set

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

sqrt (1 + (((f `2) / (f `1)) ^2)) is V28() real ext-real Element of REAL

(f `1) / (sqrt (1 + (((f `2) / (f `1)) ^2))) is V28() real ext-real Element of REAL

(f `2) / (sqrt (1 + (((f `2) / (f `1)) ^2))) is V28() real ext-real Element of REAL

|[((f `1) / (sqrt (1 + (((f `2) / (f `1)) ^2)))),((f `2) / (sqrt (1 + (((f `2) / (f `1)) ^2))))]| is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

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

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

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

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

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

C0 is Element of the carrier of f

g . C0 is set

KXP is Element of the carrier of f

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

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

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

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

KYP is V28() real ext-real set

sqrt KYP is V28() real ext-real set

K20( the carrier of f,REAL) is set

K19(K20( the carrier of f,REAL)) is set

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

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

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

K19( the carrier of f) is set

KXN is Element of the carrier of f

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

KYP is V162() V163() V164() Element of K19( the carrier of R^1)

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

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

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

KYN - I is V28() real ext-real Element of REAL

KYN + I is V28() real ext-real Element of REAL

].(KYN - I),(KYN + I).[ is V162() V163() V164() Element of K19(REAL)

min (I,1) is V28() real ext-real set

KYN - (min (I,1)) is V28() real ext-real Element of REAL

KYN + (min (I,1)) is V28() real ext-real Element of REAL

].(KYN - (min (I,1))),(KYN + (min (I,1))).[ is V162() V163() V164() Element of K19(REAL)

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

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

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

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

gg is V28() real ext-real set

gg is V28() real ext-real set

2 * KYN is V28() real ext-real Element of REAL

(2 * KYN) * (min (I,1)) is V28() real ext-real Element of REAL

(min (I,1)) ^2 is V28() real ext-real set

(min (I,1)) * (min (I,1)) is V28() real ext-real set

((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2) is V28() real ext-real Element of REAL

0 + 0 is Function-like functional empty V28() real ext-real non positive non negative V162() V163() V164() V165() V166() V167() V168() Element of REAL

(min (I,1)) * (KYN - (min (I,1))) is V28() real ext-real Element of REAL

O - ((min (I,1)) * (KYN - (min (I,1)))) is V28() real ext-real Element of REAL

O + ((min (I,1)) * (KYN - (min (I,1)))) is V28() real ext-real Element of REAL

].(O - ((min (I,1)) * (KYN - (min (I,1))))),(O + ((min (I,1)) * (KYN - (min (I,1))))).[ is V162() V163() V164() Element of K19(REAL)

ff is V162() V163() V164() Element of K19( the carrier of R^1)

y is Element of K19( the carrier of f)

g .: y is V162() V163() V164() Element of K19( the carrier of R^1)

1 / 2 is V28() real ext-real non negative Element of REAL

(1 / 2) * (min (I,1)) is V28() real ext-real Element of REAL

KYN - ((1 / 2) * (min (I,1))) is V28() real ext-real Element of REAL

(KYN - ((1 / 2) * (min (I,1)))) ^2 is V28() real ext-real Element of REAL

(KYN - ((1 / 2) * (min (I,1)))) * (KYN - ((1 / 2) * (min (I,1)))) is V28() real ext-real set

x2 is V28() real ext-real set

(min (I,1)) * KYN is V28() real ext-real Element of REAL

KYN * (min (I,1)) is V28() real ext-real Element of REAL

(KYN * (min (I,1))) + (KYN * (min (I,1))) is V28() real ext-real Element of REAL

0 + (KYN * (min (I,1))) is V28() real ext-real Element of REAL

((2 * KYN) * (min (I,1))) - ((min (I,1)) * (min (I,1))) is V28() real ext-real Element of REAL

((min (I,1)) * KYN) - ((min (I,1)) * (min (I,1))) is V28() real ext-real Element of REAL

- ((min (I,1)) * (KYN - (min (I,1)))) is V28() real ext-real Element of REAL

((2 * KYN) * (min (I,1))) - ((min (I,1)) ^2) is V28() real ext-real Element of REAL

- (((2 * KYN) * (min (I,1))) - ((min (I,1)) ^2)) is V28() real ext-real Element of REAL

O + (- ((min (I,1)) * (KYN - (min (I,1))))) is V28() real ext-real Element of REAL

(KYN ^2) + (- (((2 * KYN) * (min (I,1))) - ((min (I,1)) ^2))) is V28() real ext-real Element of REAL

sqrt (O - ((min (I,1)) * (KYN - (min (I,1))))) is V28() real ext-real Element of REAL

(KYN - (min (I,1))) ^2 is V28() real ext-real Element of REAL

(KYN - (min (I,1))) * (KYN - (min (I,1))) is V28() real ext-real set

sqrt ((KYN - (min (I,1))) ^2) is V28() real ext-real Element of REAL

2 * ((min (I,1)) * (min (I,1))) is V28() real ext-real Element of REAL

((2 * KYN) * (min (I,1))) + (2 * ((min (I,1)) * (min (I,1)))) is V28() real ext-real Element of REAL

((min (I,1)) * KYN) + 0 is V28() real ext-real Element of REAL

((2 * KYN) * (min (I,1))) + ((min (I,1)) * (min (I,1))) is V28() real ext-real Element of REAL

(((2 * KYN) * (min (I,1))) + ((min (I,1)) * (min (I,1)))) + ((min (I,1)) * (min (I,1))) is V28() real ext-real Element of REAL

(((min (I,1)) * KYN) - ((min (I,1)) * (min (I,1)))) + ((min (I,1)) * (min (I,1))) is V28() real ext-real Element of REAL

(KYN ^2) + (((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2)) is V28() real ext-real Element of REAL

(KYN + (min (I,1))) ^2 is V28() real ext-real Element of REAL

(KYN + (min (I,1))) * (KYN + (min (I,1))) is V28() real ext-real set

sqrt ((KYN + (min (I,1))) ^2) is V28() real ext-real Element of REAL

sqrt (O + ((min (I,1)) * (KYN - (min (I,1))))) is V28() real ext-real Element of REAL

x2 is V28() real ext-real set

(KYN ^2) - (((min (I,1)) * KYN) - ((min (I,1)) * (min (I,1)))) is V28() real ext-real Element of REAL

4 is non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT

3 / 4 is V28() real ext-real non negative Element of REAL

(3 / 4) * ((min (I,1)) ^2) is V28() real ext-real Element of REAL

((KYN - ((1 / 2) * (min (I,1)))) ^2) + ((3 / 4) * ((min (I,1)) ^2)) is V28() real ext-real Element of REAL

x2 is V28() real ext-real set

KXP .: y is V162() V163() V164() Element of K19( the carrier of R^1)

x2 is set

dom KXP is Element of K19( the carrier of f)

px is set

KXP . px is set

q is Element of the carrier of f

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

dom g is Element of K19( the carrier of f)

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

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

p4 is V28() real ext-real set

(((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2)) / 3 is V28() real ext-real Element of REAL

O - ((((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2)) / 3) is V28() real ext-real Element of REAL

O + ((((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2)) / 3) is V28() real ext-real Element of REAL

].(O - ((((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2)) / 3)),(O + ((((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2)) / 3)).[ is V162() V163() V164() Element of K19(REAL)

ff is V162() V163() V164() Element of K19( the carrier of R^1)

y is Element of K19( the carrier of f)

g .: y is V162() V163() V164() Element of K19( the carrier of R^1)

(KYN ^2) + (((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2)) is V28() real ext-real Element of REAL

sqrt (O + ((((2 * KYN) * (min (I,1))) + ((min (I,1)) ^2)) / 3)) is V28() real ext-real Element of REAL

(KYN + (min (I,1))) ^2 is V28() real ext-real Element of REAL

(KYN + (min (I,1))) * (KYN + (min (I,1))) is V28() real ext-real set

sqrt ((KYN + (min (I,1))) ^2) is V28() real ext-real Element of REAL

x2 is V28() real ext-real set

KXP .: y is V162() V163() V164() Element of K19( the carrier of R^1)

x2 is set

dom KXP is Element of K19( the carrier of f)

px is set

KXP . px is set

q is Element of the carrier of f

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

dom g is Element of K19( the carrier of f)

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

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

p4 is V28() real ext-real set

p4 is V28() real ext-real set

KXN is Element of the carrier of f

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

KYP is V28() real ext-real set

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

sqrt KYP is V28() real ext-real set

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

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

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

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

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

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

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

KYP is Element of the carrier of f

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

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

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

KYN is V28() real ext-real set

O is V28() real ext-real set

KYN / O is V28() real ext-real set

(KYN / O) ^2 is V28() real ext-real set

(KYN / O) * (KYN / O) is V28() real ext-real set

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

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

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

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

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

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

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

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

KYP is Element of the carrier of f

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

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

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

KYN is V28() real ext-real set

O is V28() real ext-real set

KYN / O is V28() real ext-real set

(KYN / O) ^2 is V28() real ext-real set

(KYN / O) * (KYN / O) is V28() real ext-real set

1 + ((KYN / O) ^2) is V28() real ext-real Element of REAL

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

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

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

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

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

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

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

KXN is Element of the carrier of f

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

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

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

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

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

KYP / KYN is V28() real ext-real Element of REAL

(KYP / KYN) ^2 is V28() real ext-real Element of REAL

(KYP / KYN) * (KYP / KYN) is V28() real ext-real set

1 + ((KYP / KYN) ^2) is V28() real ext-real Element of REAL

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

KYP is Element of the carrier of f

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

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

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

KYN is V28() real ext-real set

O is V28() real ext-real set

KYN / O is V28() real ext-real set

(KYN / O) ^2 is V28() real ext-real set

(KYN / O) * (KYN / O) is V28() real ext-real set

1 + ((KYN / O) ^2) is V28() real ext-real Element of REAL

sqrt (1 + ((KYN / O) ^2)) is V28() real ext-real Element of REAL

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

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

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

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

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

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

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

KXN is Element of the carrier of f

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

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

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

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

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

KYP / KYN is V28() real ext-real Element of REAL

(KYP / KYN) ^2 is V28() real ext-real Element of REAL

(KYP / KYN) * (KYP / KYN) is V28() real ext-real set

1 + ((KYP / KYN) ^2) is V28() real ext-real Element of REAL

sqrt (1 + ((KYP / KYN) ^2)) is V28() real ext-real Element of REAL

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

KYP is Element of the carrier of f

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

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

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

KYN is V28() real ext-real set

O is V28() real ext-real set

KYN / O is V28() real ext-real set

(KYN / O) ^2 is V28() real ext-real set

(KYN / O) * (KYN / O) is V28() real ext-real set

1 + ((KYN / O) ^2) is V28() real ext-real Element of REAL

sqrt (1 + ((KYN / O) ^2)) is V28() real ext-real Element of REAL

KYN / (sqrt (1 + ((KYN / O) ^2))) is V28() real ext-real Element of REAL

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

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

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

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

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

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

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

KXN is Element of the carrier of f

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

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

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

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

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

KYP / KYN is V28() real ext-real Element of REAL

(KYP / KYN) ^2 is V28() real ext-real Element of REAL

(KYP / KYN) * (KYP / KYN) is V28() real ext-real set

1 + ((KYP / KYN) ^2) is V28() real ext-real Element of REAL

sqrt (1 + ((KYP / KYN) ^2)) is V28() real ext-real Element of REAL

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

KYP is Element of the carrier of f

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

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

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

KYN is V28() real ext-real set

O is V28() real ext-real set

KYN / O is V28() real ext-real set

(KYN / O) ^2 is V28() real ext-real set

(KYN / O) * (KYN / O) is V28() real ext-real set

1 + ((KYN / O) ^2) is V28() real ext-real Element of REAL

sqrt (1 + ((KYN / O) ^2)) is V28() real ext-real Element of REAL

O / (sqrt (1 + ((KYN / O) ^2))) is V28() real ext-real Element of REAL

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

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

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

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

g is Element of the carrier of ((TOP-REAL 2) | f)

(proj2 | f) . g is V28() real ext-real Element of REAL

proj2 . g is set

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

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

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

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

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

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

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

C0 is Element of the carrier of ((TOP-REAL 2) | f)

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

proj2 . C0 is set

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

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

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

g is Element of the carrier of ((TOP-REAL 2) | f)

(proj1 | f) . g is V28() real ext-real Element of REAL

proj1 . g is set

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

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

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

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

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

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

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

C0 is Element of the carrier of ((TOP-REAL 2) | f)

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

proj1 . C0 is set

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

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

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

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

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

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

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

KXN is Element of the carrier of ((TOP-REAL 2) | f)

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

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

proj1 . KXN is set

KYP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

dom g is Element of K19( the carrier of ((TOP-REAL 2) | f))

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

KYP is set

g . KYP is set

KXN . KYP is set

O is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

proj1 . O is V28() real ext-real Element of REAL

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

KYN is Element of the carrier of ((TOP-REAL 2) | f)

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

proj2 . KYN is set

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

proj1 . KYN is set

g . O is set

(O `2) / (O `1) is V28() real ext-real Element of REAL

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

((O `2) / (O `1)) * ((O `2) / (O `1)) is V28() real ext-real set

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

sqrt (1 + (((O `2) / (O `1)) ^2)) is V28() real ext-real Element of REAL

(O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2))) is V28() real ext-real Element of REAL

dom KXN is Element of K19( the carrier of ((TOP-REAL 2) | f))

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

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

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

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

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

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

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

KXN is Element of the carrier of ((TOP-REAL 2) | f)

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

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

proj1 . KXN is set

KYP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

dom g is Element of K19( the carrier of ((TOP-REAL 2) | f))

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

KYP is set

g . KYP is set

KXN . KYP is set

O is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

proj1 . O is V28() real ext-real Element of REAL

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

KYN is Element of the carrier of ((TOP-REAL 2) | f)

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

proj2 . KYN is set

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

proj1 . KYN is set

g . O is set

(O `2) / (O `1) is V28() real ext-real Element of REAL

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

((O `2) / (O `1)) * ((O `2) / (O `1)) is V28() real ext-real set

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

sqrt (1 + (((O `2) / (O `1)) ^2)) is V28() real ext-real Element of REAL

(O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2))) is V28() real ext-real Element of REAL

dom KXN is Element of K19( the carrier of ((TOP-REAL 2) | f))

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

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

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

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

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

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

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

KXN is Element of the carrier of ((TOP-REAL 2) | f)

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

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

proj2 . KXN is set

KYP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

dom g is Element of K19( the carrier of ((TOP-REAL 2) | f))

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

KYP is set

g . KYP is set

KXN . KYP is set

O is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

proj1 . O is V28() real ext-real Element of REAL

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

KYN is Element of the carrier of ((TOP-REAL 2) | f)

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

proj2 . KYN is set

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

proj1 . KYN is set

g . O is set

(O `1) / (O `2) is V28() real ext-real Element of REAL

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

((O `1) / (O `2)) * ((O `1) / (O `2)) is V28() real ext-real set

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

sqrt (1 + (((O `1) / (O `2)) ^2)) is V28() real ext-real Element of REAL

(O `2) / (sqrt (1 + (((O `1) / (O `2)) ^2))) is V28() real ext-real Element of REAL

dom KXN is Element of K19( the carrier of ((TOP-REAL 2) | f))

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

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

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

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

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

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

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

KXN is Element of the carrier of ((TOP-REAL 2) | f)

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

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

proj2 . KXN is set

KYP is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

dom g is Element of K19( the carrier of ((TOP-REAL 2) | f))

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

KYP is set

g . KYP is set

KXN . KYP is set

O is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

proj1 . O is V28() real ext-real Element of REAL

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

KYN is Element of the carrier of ((TOP-REAL 2) | f)

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

proj2 . KYN is set

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

proj1 . KYN is set

g . O is set

(O `1) / (O `2) is V28() real ext-real Element of REAL

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

((O `1) / (O `2)) * ((O `1) / (O `2)) is V28() real ext-real set

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

sqrt (1 + (((O `1) / (O `2)) ^2)) is V28() real ext-real Element of REAL

(O `1) / (sqrt (1 + (((O `1) / (O `2)) ^2))) is V28() real ext-real Element of REAL

dom KXN is Element of K19( the carrier of ((TOP-REAL 2) | f))

0.REAL 2 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

g is set

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

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

() . g is Relation-like Function-like set

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

(() | f) . g is Relation-like Function-like set

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

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

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

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

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

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

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

(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2

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

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

g is set

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

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

() . g is Relation-like Function-like set