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
{ b1 where b1 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2) : b1 `2 <= b1 `1 } is set
{ b1 where b1 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2) : b1 `1 <= b1 `2 } is set
{ b1 where b1 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2) : - (b1 `1) <= b1 `2 } is set
{ b1 where b1 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2) : b1 `2 <= - (b1 `1) } is set
{ b1 where b1 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2) : - (b1 `2) <= b1 `1 } is set
{ b1 where b1 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2) : b1 `1 <= - (b1 `2) } is set
R^2-unit_square is functional non empty compact being_simple_closed_curve Element of K19( the carrier of (TOP-REAL 2))
{ b1 where b1 is Relation-like Function-like V43(2) V111() V154() Element of the carrier of (TOP-REAL 2) : ( ( b1 `1 = 0 & b1 `2 <= 1 & 0 <= b1 `2 ) or ( b1 `1 <= 1 & 0 <= b1 `1 & b1 `2 = 1 ) or ( b1 `1 <= 1 & 0 <= b1 `1 & b1 `2 = 0 ) or ( b1 `1 = 1 & b1 `2 <= 1 & 0 <= b1 `2 ) ) } is set
(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