REAL is V142() V143() V144() V148() V201() V202() V204() set
NAT is V142() V143() V144() V145() V146() V147() V148() V201() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V142() V148() set
omega is V142() V143() V144() V145() V146() V147() V148() V201() set
K6(omega) is set
K6(NAT) is set
1 is non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() V199() V201() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() V199() V201() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
RAT is V142() V143() V144() V145() V148() set
INT is V142() V143() V144() V145() V146() V148() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty functional set
K6( the carrier of (TOP-REAL 2)) is set
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2))) is set
K448() is non empty strict TopSpace-like V196() TopStruct
the carrier of K448() is non empty V142() V143() V144() set
RealSpace is non empty strict Reflexive discerning V91() triangle Discerning V196() MetrStruct
R^1 is non empty strict TopSpace-like V196() TopStruct
the carrier of R^1 is non empty V142() V143() V144() set
K7( the carrier of (TOP-REAL 2),REAL) is set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
0 is empty Function-like functional V142() V143() V144() V145() V146() V147() V148() V201() V204() set
K6( the carrier of R^1) is set
0 is empty natural V11() real ext-real non positive non negative Function-like functional V79() V80() V142() V143() V144() V145() V146() V147() V148() V201() V204() Element of NAT
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V196() SubSpace of R^1
K7( the carrier of R^1, the carrier of R^1) is set
K6(K7( the carrier of R^1, the carrier of R^1)) is set
0. (TOP-REAL 2) is Relation-like Function-like V43(2) V52( TOP-REAL 2) V76() V134() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|[0,0]| is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
sqrt 1 is V11() real ext-real Element of REAL
K38(1) is V11() real ext-real non positive set
proj1 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like quasi_total Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like quasi_total Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
real_dist is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
(0. (TOP-REAL 2)) `1 is V11() real ext-real Element of REAL
(0. (TOP-REAL 2)) `2 is V11() real ext-real Element of REAL
I[01] is non empty strict TopSpace-like V196() SubSpace of R^1
the carrier of I[01] is non empty V142() V143() V144() set
K7( the carrier of I[01], the carrier of (TOP-REAL 2)) is set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2))) is set
[.0,1.] is V142() V143() V144() V204() Element of K6(REAL)
Sq_Circ is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
{ b1 where b1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : |.b1.| = 1 } is set
Sq_Circ " is Relation-like Function-like set
rng Sq_Circ is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : |.b1.| <= 1 } is set
{ b1 where b1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : ( |.b1.| = 1 & b1 `2 <= b1 `1 & - (b1 `1) <= b1 `2 ) } is set
{ b1 where b1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : ( |.b1.| = 1 & b1 `1 <= b1 `2 & b1 `2 <= - (b1 `1) ) } is set
{ b1 where b1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : ( |.b1.| = 1 & b1 `1 <= b1 `2 & - (b1 `1) <= b1 `2 ) } is set
{ b1 where b1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : ( |.b1.| = 1 & b1 `2 <= b1 `1 & b1 `2 <= - (b1 `1) ) } is set
- 1 is V11() real ext-real non positive Element of REAL
p1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|.p1.| is V11() real ext-real non negative Element of REAL
p1 `1 is V11() real ext-real Element of REAL
p1 `2 is V11() real ext-real Element of REAL
|.p1.| ^2 is V11() real ext-real Element of REAL
K37(|.p1.|,|.p1.|) is V11() real ext-real non negative set
(p1 `1) ^2 is V11() real ext-real Element of REAL
K37((p1 `1),(p1 `1)) is V11() real ext-real set
(p1 `2) ^2 is V11() real ext-real Element of REAL
K37((p1 `2),(p1 `2)) is V11() real ext-real set
((p1 `1) ^2) + ((p1 `2) ^2) is V11() real ext-real Element of REAL
(|.p1.| ^2) - ((p1 `1) ^2) is V11() real ext-real Element of REAL
0 + ((p1 `1) ^2) is V11() real ext-real Element of REAL
((|.p1.| ^2) - ((p1 `1) ^2)) + ((p1 `1) ^2) is V11() real ext-real Element of REAL
- |.p1.| is V11() real ext-real non positive Element of REAL
(|.p1.| ^2) - ((p1 `2) ^2) is V11() real ext-real Element of REAL
0 + ((p1 `2) ^2) is V11() real ext-real Element of REAL
((|.p1.| ^2) - ((p1 `2) ^2)) + ((p1 `2) ^2) is V11() real ext-real Element of REAL
p1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|.p1.| is V11() real ext-real non negative Element of REAL
p1 `1 is V11() real ext-real Element of REAL
p1 `2 is V11() real ext-real Element of REAL
|.p1.| ^2 is V11() real ext-real Element of REAL
K37(|.p1.|,|.p1.|) is V11() real ext-real non negative set
(p1 `1) ^2 is V11() real ext-real Element of REAL
K37((p1 `1),(p1 `1)) is V11() real ext-real set
(p1 `2) ^2 is V11() real ext-real Element of REAL
K37((p1 `2),(p1 `2)) is V11() real ext-real set
((p1 `1) ^2) + ((p1 `2) ^2) is V11() real ext-real Element of REAL
(|.p1.| ^2) - ((p1 `1) ^2) is V11() real ext-real Element of REAL
((|.p1.| ^2) - ((p1 `1) ^2)) + ((p1 `1) ^2) is V11() real ext-real Element of REAL
0 + ((p1 `1) ^2) is V11() real ext-real Element of REAL
- |.p1.| is V11() real ext-real non positive Element of REAL
(|.p1.| ^2) - ((p1 `2) ^2) is V11() real ext-real Element of REAL
((|.p1.| ^2) - ((p1 `2) ^2)) + ((p1 `2) ^2) is V11() real ext-real Element of REAL
0 + ((p1 `2) ^2) is V11() real ext-real Element of REAL
p3 is V11() real ext-real Element of REAL
p1 is V11() real ext-real Element of REAL
p2 is V11() real ext-real Element of REAL
p4 is V11() real ext-real Element of REAL
Closed-Interval-MSpace (p1,p2) is non empty strict Reflexive discerning V91() triangle Discerning SubSpace of RealSpace
Closed-Interval-MSpace (p3,p4) is non empty strict Reflexive discerning V91() triangle Discerning SubSpace of RealSpace
P is V11() real ext-real Element of REAL
C0 is non empty MetrStruct
the carrier of C0 is non empty set
f is non empty MetrStruct
the carrier of f is non empty set
g is Element of the carrier of C0
Ball (g,P) is Element of K6( the carrier of C0)
K6( the carrier of C0) is set
h is Element of the carrier of f
Ball (h,P) is Element of K6( the carrier of f)
K6( the carrier of f) is set
[.p3,p4.] is V142() V143() V144() V204() Element of K6(REAL)
f2 is set
{ b1 where b1 is Element of the carrier of C0 : not P <= dist (g,b1) } is set
g2 is Element of the carrier of C0
dist (g,g2) is V11() real ext-real Element of REAL
[.p1,p2.] is V142() V143() V144() V204() Element of K6(REAL)
the distance of C0 is Relation-like K7( the carrier of C0, the carrier of C0) -defined REAL -valued Function-like quasi_total Element of K6(K7(K7( the carrier of C0, the carrier of C0),REAL))
K7( the carrier of C0, the carrier of C0) is set
K7(K7( the carrier of C0, the carrier of C0),REAL) is set
K6(K7(K7( the carrier of C0, the carrier of C0),REAL)) is set
the distance of C0 . (g,g2) is V11() real ext-real Element of REAL
real_dist . (g,g2) is set
the distance of f is Relation-like K7( the carrier of f, the carrier of f) -defined REAL -valued Function-like quasi_total Element of K6(K7(K7( the carrier of f, the carrier of f),REAL))
K7( the carrier of f, the carrier of f) is set
K7(K7( the carrier of f, the carrier of f),REAL) is set
K6(K7(K7( the carrier of f, the carrier of f),REAL)) is set
h1 is Element of the carrier of f
the distance of f . (h,h1) is V11() real ext-real Element of REAL
dist (h,h1) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of f : not P <= dist (h,b1) } is set
K6( the carrier of I[01]) is set
p1 is V11() real ext-real set
p2 is V11() real ext-real set
p3 is V142() V143() V144() Element of K6( the carrier of I[01])
[.p1,p2.] is V142() V143() V144() V204() Element of K6(REAL)
Closed-Interval-TSpace (p1,p2) is non empty strict TopSpace-like V196() SubSpace of R^1
I[01] | p3 is strict TopSpace-like V196() SubSpace of I[01]
p1 is TopStruct
the carrier of p1 is set
p2 is non empty TopStruct
the carrier of p2 is non empty set
K7( the carrier of p1, the carrier of p2) is set
K6(K7( the carrier of p1, the carrier of p2)) is set
p3 is non empty TopStruct
the carrier of p3 is non empty set
K7( the carrier of p2, the carrier of p3) is set
K6(K7( the carrier of p2, the carrier of p3)) is set
p4 is Relation-like the carrier of p1 -defined the carrier of p2 -valued Function-like V29( the carrier of p1) quasi_total Element of K6(K7( the carrier of p1, the carrier of p2))
P is non empty Relation-like the carrier of p2 -defined the carrier of p3 -valued Function-like V29( the carrier of p2) quasi_total Element of K6(K7( the carrier of p2, the carrier of p3))
P * p4 is Relation-like the carrier of p1 -defined the carrier of p3 -valued Function-like V29( the carrier of p1) quasi_total Element of K6(K7( the carrier of p1, the carrier of p3))
K7( the carrier of p1, the carrier of p3) is set
K6(K7( the carrier of p1, the carrier of p3)) is set
p1 is TopStruct
the carrier of p1 is set
p2 is TopStruct
the carrier of p2 is set
K7( the carrier of p1, the carrier of p2) is set
K6(K7( the carrier of p1, the carrier of p2)) is set
p3 is TopStruct
the carrier of p3 is set
K7( the carrier of p2, the carrier of p3) is set
K6(K7( the carrier of p2, the carrier of p3)) is set
p4 is Relation-like the carrier of p1 -defined the carrier of p2 -valued Function-like quasi_total Element of K6(K7( the carrier of p1, the carrier of p2))
P is Relation-like the carrier of p2 -defined the carrier of p3 -valued Function-like quasi_total Element of K6(K7( the carrier of p2, the carrier of p3))
P * p4 is Relation-like the carrier of p1 -defined the carrier of p3 -valued Function-like Element of K6(K7( the carrier of p1, the carrier of p3))
K7( the carrier of p1, the carrier of p3) is set
K6(K7( the carrier of p1, the carrier of p3)) is set
p1 is TopStruct
the carrier of p1 is set
p2 is non empty TopStruct
the carrier of p2 is non empty set
K6( the carrier of p2) is set
p3 is non empty TopStruct
the carrier of p3 is non empty set
K7( the carrier of p2, the carrier of p3) is set
K6(K7( the carrier of p2, the carrier of p3)) is set
K7( the carrier of p1, the carrier of p3) is set
K6(K7( the carrier of p1, the carrier of p3)) is set
p4 is non empty Element of K6( the carrier of p2)
p2 | p4 is non empty strict SubSpace of p2
the carrier of (p2 | p4) is non empty set
K7( the carrier of p1, the carrier of (p2 | p4)) is set
K6(K7( the carrier of p1, the carrier of (p2 | p4))) is set
P is Relation-like the carrier of p1 -defined the carrier of (p2 | p4) -valued Function-like V29( the carrier of p1) quasi_total Element of K6(K7( the carrier of p1, the carrier of (p2 | p4)))
C0 is non empty Relation-like the carrier of p2 -defined the carrier of p3 -valued Function-like V29( the carrier of p2) quasi_total Element of K6(K7( the carrier of p2, the carrier of p3))
C0 * P is Relation-like the carrier of p1 -defined the carrier of p3 -valued Function-like Element of K6(K7( the carrier of p1, the carrier of p3))
f is Relation-like the carrier of p1 -defined the carrier of p3 -valued Function-like V29( the carrier of p1) quasi_total Element of K6(K7( the carrier of p1, the carrier of p3))
K6( the carrier of p3) is set
g is Element of K6( the carrier of p3)
(C0 * P) " g is Element of K6( the carrier of p1)
K6( the carrier of p1) is set
C0 " g is Element of K6( the carrier of p2)
P " (C0 " g) is Element of K6( the carrier of p1)
K6( the carrier of (p2 | p4)) is set
p4 /\ (C0 " g) is Element of K6( the carrier of p2)
rng P is Element of K6( the carrier of (p2 | p4))
(rng P) /\ the carrier of (p2 | p4) is Element of K6( the carrier of (p2 | p4))
[#] (p2 | p4) is non empty non proper Element of K6( the carrier of (p2 | p4))
h is Element of K6( the carrier of (p2 | p4))
f " g is Element of K6( the carrier of p1)
(rng P) /\ (C0 " g) is Element of K6( the carrier of p2)
P " ((rng P) /\ (C0 " g)) is Element of K6( the carrier of p1)
the carrier of (p2 | p4) /\ (C0 " g) is Element of K6( the carrier of p2)
(rng P) /\ ( the carrier of (p2 | p4) /\ (C0 " g)) is Element of K6( the carrier of p2)
P " ((rng P) /\ ( the carrier of (p2 | p4) /\ (C0 " g))) is Element of K6( the carrier of p1)
P " h is Element of K6( the carrier of p1)
p1 is V11() real ext-real Element of REAL
p2 is V11() real ext-real Element of REAL
Closed-Interval-TSpace (p1,p2) is non empty strict TopSpace-like V196() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (p1,p2)) is non empty V142() V143() V144() set
p3 is V11() real ext-real Element of REAL
p4 is V11() real ext-real Element of REAL
Closed-Interval-TSpace (p3,p4) is non empty strict TopSpace-like V196() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (p3,p4)) is non empty V142() V143() V144() set
K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4)))) is set
P is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
C0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
[.p1,p2.] is V142() V143() V144() V204() Element of K6(REAL)
h is non empty Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like V29( the carrier of (Closed-Interval-TSpace (p1,p2))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
h . P is set
h . C0 is set
h . p2 is set
[.p3,p4.] is V142() V143() V144() V204() Element of K6(REAL)
f2 is non empty V142() V143() V144() Element of K6( the carrier of R^1)
R^1 | f2 is non empty strict TopSpace-like V196() SubSpace of R^1
K6( the carrier of (Closed-Interval-TSpace (p1,p2))) is set
[.P,p2.] is V142() V143() V144() V204() Element of K6(REAL)
dom h is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
[#] (Closed-Interval-TSpace (p1,p2)) is non empty non proper closed V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
[.C0,P.] is V142() V143() V144() V204() Element of K6(REAL)
h1 is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
(Closed-Interval-TSpace (p1,p2)) | h1 is strict TopSpace-like V196() SubSpace of Closed-Interval-TSpace (p1,p2)
the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1) is V142() V143() V144() set
K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1), the carrier of (Closed-Interval-TSpace (p3,p4))) is set
K6(K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1), the carrier of (Closed-Interval-TSpace (p3,p4)))) is set
O is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
h | O is Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
Closed-Interval-TSpace (C0,P) is non empty strict TopSpace-like V196() SubSpace of R^1
I is Relation-like the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like V29( the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1)) quasi_total Element of K6(K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1), the carrier of (Closed-Interval-TSpace (p3,p4))))
the carrier of (Closed-Interval-TSpace (C0,P)) is non empty V142() V143() V144() set
K7( the carrier of (Closed-Interval-TSpace (C0,P)), the carrier of R^1) is set
K6(K7( the carrier of (Closed-Interval-TSpace (C0,P)), the carrier of R^1)) is set
h | h1 is Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
KXP is non empty Relation-like the carrier of (Closed-Interval-TSpace (C0,P)) -defined the carrier of R^1 -valued Function-like V29( the carrier of (Closed-Interval-TSpace (C0,P))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (C0,P)), the carrier of R^1))
KXP . C0 is set
f + g is V11() real ext-real Element of REAL
(f + g) / 2 is V11() real ext-real Element of REAL
f + f is V11() real ext-real Element of REAL
2 * f is V11() real ext-real Element of REAL
(2 * f) / 2 is V11() real ext-real Element of REAL
dom KXP is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (C0,P)))
K6( the carrier of (Closed-Interval-TSpace (C0,P))) is set
rng I is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p3,p4)))
K6( the carrier of (Closed-Interval-TSpace (p3,p4))) is set
g + g is V11() real ext-real Element of REAL
2 * g is V11() real ext-real Element of REAL
(2 * g) / 2 is V11() real ext-real Element of REAL
g2 is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
(Closed-Interval-TSpace (p1,p2)) | g2 is strict TopSpace-like V196() SubSpace of Closed-Interval-TSpace (p1,p2)
the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2) is V142() V143() V144() set
K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2), the carrier of (Closed-Interval-TSpace (p3,p4))) is set
K6(K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2), the carrier of (Closed-Interval-TSpace (p3,p4)))) is set
KYP is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
h | KYP is Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
Closed-Interval-TSpace (P,p2) is non empty strict TopSpace-like V196() SubSpace of R^1
KYN is Relation-like the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like V29( the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2)) quasi_total Element of K6(K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2), the carrier of (Closed-Interval-TSpace (p3,p4))))
the carrier of (Closed-Interval-TSpace (P,p2)) is non empty V142() V143() V144() set
K7( the carrier of (Closed-Interval-TSpace (P,p2)), the carrier of R^1) is set
K6(K7( the carrier of (Closed-Interval-TSpace (P,p2)), the carrier of R^1)) is set
h | g2 is Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
x2 is non empty Relation-like the carrier of (Closed-Interval-TSpace (P,p2)) -defined the carrier of R^1 -valued Function-like V29( the carrier of (Closed-Interval-TSpace (P,p2))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (P,p2)), the carrier of R^1))
x2 . p2 is set
x2 . P is set
z3 is V11() real ext-real Element of REAL
x2 . z3 is set
KXP . P is set
z2 is V11() real ext-real Element of REAL
KXP . z2 is set
h . z2 is set
h . z3 is set
p1 is V11() real ext-real Element of REAL
p2 is V11() real ext-real Element of REAL
Closed-Interval-TSpace (p1,p2) is non empty strict TopSpace-like V196() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (p1,p2)) is non empty V142() V143() V144() set
p3 is V11() real ext-real Element of REAL
p4 is V11() real ext-real Element of REAL
Closed-Interval-TSpace (p3,p4) is non empty strict TopSpace-like V196() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (p3,p4)) is non empty V142() V143() V144() set
K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4)))) is set
P is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
C0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
[.p1,p2.] is V142() V143() V144() V204() Element of K6(REAL)
h is non empty Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like V29( the carrier of (Closed-Interval-TSpace (p1,p2))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
h . P is set
h . C0 is set
h . p2 is set
[.p3,p4.] is V142() V143() V144() V204() Element of K6(REAL)
f2 is non empty V142() V143() V144() Element of K6( the carrier of R^1)
R^1 | f2 is non empty strict TopSpace-like V196() SubSpace of R^1
K6( the carrier of (Closed-Interval-TSpace (p1,p2))) is set
[.P,p2.] is V142() V143() V144() V204() Element of K6(REAL)
dom h is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
[#] (Closed-Interval-TSpace (p1,p2)) is non empty non proper closed V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
[.C0,P.] is V142() V143() V144() V204() Element of K6(REAL)
h1 is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
(Closed-Interval-TSpace (p1,p2)) | h1 is strict TopSpace-like V196() SubSpace of Closed-Interval-TSpace (p1,p2)
the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1) is V142() V143() V144() set
K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1), the carrier of (Closed-Interval-TSpace (p3,p4))) is set
K6(K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1), the carrier of (Closed-Interval-TSpace (p3,p4)))) is set
O is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
h | O is Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
Closed-Interval-TSpace (C0,P) is non empty strict TopSpace-like V196() SubSpace of R^1
I is Relation-like the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like V29( the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1)) quasi_total Element of K6(K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | h1), the carrier of (Closed-Interval-TSpace (p3,p4))))
the carrier of (Closed-Interval-TSpace (C0,P)) is non empty V142() V143() V144() set
K7( the carrier of (Closed-Interval-TSpace (C0,P)), the carrier of R^1) is set
K6(K7( the carrier of (Closed-Interval-TSpace (C0,P)), the carrier of R^1)) is set
h | h1 is Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
KXP is non empty Relation-like the carrier of (Closed-Interval-TSpace (C0,P)) -defined the carrier of R^1 -valued Function-like V29( the carrier of (Closed-Interval-TSpace (C0,P))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (C0,P)), the carrier of R^1))
KXP . C0 is set
f + g is V11() real ext-real Element of REAL
(f + g) / 2 is V11() real ext-real Element of REAL
f + f is V11() real ext-real Element of REAL
2 * f is V11() real ext-real Element of REAL
(2 * f) / 2 is V11() real ext-real Element of REAL
dom KXP is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (C0,P)))
K6( the carrier of (Closed-Interval-TSpace (C0,P))) is set
rng I is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p3,p4)))
K6( the carrier of (Closed-Interval-TSpace (p3,p4))) is set
g + g is V11() real ext-real Element of REAL
2 * g is V11() real ext-real Element of REAL
(2 * g) / 2 is V11() real ext-real Element of REAL
g2 is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
(Closed-Interval-TSpace (p1,p2)) | g2 is strict TopSpace-like V196() SubSpace of Closed-Interval-TSpace (p1,p2)
the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2) is V142() V143() V144() set
K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2), the carrier of (Closed-Interval-TSpace (p3,p4))) is set
K6(K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2), the carrier of (Closed-Interval-TSpace (p3,p4)))) is set
KYP is V142() V143() V144() Element of K6( the carrier of (Closed-Interval-TSpace (p1,p2)))
h | KYP is Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
Closed-Interval-TSpace (P,p2) is non empty strict TopSpace-like V196() SubSpace of R^1
KYN is Relation-like the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like V29( the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2)) quasi_total Element of K6(K7( the carrier of ((Closed-Interval-TSpace (p1,p2)) | g2), the carrier of (Closed-Interval-TSpace (p3,p4))))
the carrier of (Closed-Interval-TSpace (P,p2)) is non empty V142() V143() V144() set
K7( the carrier of (Closed-Interval-TSpace (P,p2)), the carrier of R^1) is set
K6(K7( the carrier of (Closed-Interval-TSpace (P,p2)), the carrier of R^1)) is set
h | g2 is Relation-like the carrier of (Closed-Interval-TSpace (p1,p2)) -defined the carrier of (Closed-Interval-TSpace (p3,p4)) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (p1,p2)), the carrier of (Closed-Interval-TSpace (p3,p4))))
x2 is non empty Relation-like the carrier of (Closed-Interval-TSpace (P,p2)) -defined the carrier of R^1 -valued Function-like V29( the carrier of (Closed-Interval-TSpace (P,p2))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (P,p2)), the carrier of R^1))
x2 . p2 is set
x2 . P is set
z3 is V11() real ext-real Element of REAL
x2 . z3 is set
KXP . P is set
z2 is V11() real ext-real Element of REAL
KXP . z2 is set
h . z2 is set
h . z3 is set
p1 is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() V201() Element of NAT
TOP-REAL p1 is non empty TopSpace-like T_0 T_1 T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict RLTopStruct
0. (TOP-REAL p1) is Relation-like Function-like V43(p1) V52( TOP-REAL p1) V76() V134() Element of the carrier of (TOP-REAL p1)
the carrier of (TOP-REAL p1) is non empty functional set
the ZeroF of (TOP-REAL p1) is Relation-like Function-like V43(p1) V76() V134() Element of the carrier of (TOP-REAL p1)
- (0. (TOP-REAL p1)) is Relation-like Function-like V43(p1) V76() V134() Element of the carrier of (TOP-REAL p1)
(0. (TOP-REAL p1)) + (0. (TOP-REAL p1)) is Relation-like Function-like V43(p1) V76() V134() Element of the carrier of (TOP-REAL p1)
p1 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
p2 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng p1 is functional Element of K6( the carrier of (TOP-REAL 2))
rng p2 is functional Element of K6( the carrier of (TOP-REAL 2))
p3 is V11() real ext-real Element of REAL
p4 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
C0 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of the carrier of I[01]
g is V11() real ext-real Element of the carrier of I[01]
p1 . f is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(p1 . f) `1 is V11() real ext-real Element of REAL
(p1 . f) `2 is V11() real ext-real Element of REAL
p1 . g is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(p1 . g) `1 is V11() real ext-real Element of REAL
(p1 . g) `2 is V11() real ext-real Element of REAL
p2 . f is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(p2 . f) `2 is V11() real ext-real Element of REAL
(p2 . f) `1 is V11() real ext-real Element of REAL
p2 . g is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(p2 . g) `2 is V11() real ext-real Element of REAL
(p2 . g) `1 is V11() real ext-real Element of REAL
p1 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
p1 . 1 is Relation-like Function-like set
p1 . 0 is Relation-like Function-like set
rng p1 is functional Element of K6( the carrier of (TOP-REAL 2))
dom p1 is V142() V143() V144() Element of K6( the carrier of I[01])
p2 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p2 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p2) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p2)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p2))) is set
p3 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p2)))
P is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p2)))
P . 0 is set
P . 1 is set
rng P is Element of K6( the carrier of ((TOP-REAL 2) | p2))
K6( the carrier of ((TOP-REAL 2) | p2)) is set
[#] ((TOP-REAL 2) | p2) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p2))
C0 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
p1 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
p2 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng p1 is functional Element of K6( the carrier of (TOP-REAL 2))
rng p2 is functional Element of K6( the carrier of (TOP-REAL 2))
p3 is functional Element of K6( the carrier of (TOP-REAL 2))
p4 is functional Element of K6( the carrier of (TOP-REAL 2))
P is functional Element of K6( the carrier of (TOP-REAL 2))
C0 is functional Element of K6( the carrier of (TOP-REAL 2))
f is functional Element of K6( the carrier of (TOP-REAL 2))
g is V11() real ext-real Element of the carrier of I[01]
h is V11() real ext-real Element of the carrier of I[01]
p1 . g is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 . h is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 . g is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 . h is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 . 1 is Relation-like Function-like set
p2 . 0 is Relation-like Function-like set
f2 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
f2 . 0 is Relation-like Function-like set
f2 . 1 is Relation-like Function-like set
rng f2 is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : 1 <= |.b1.| } is set
p1 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
p2 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng p1 is functional Element of K6( the carrier of (TOP-REAL 2))
rng p2 is functional Element of K6( the carrier of (TOP-REAL 2))
p3 is functional Element of K6( the carrier of (TOP-REAL 2))
p4 is functional Element of K6( the carrier of (TOP-REAL 2))
P is functional Element of K6( the carrier of (TOP-REAL 2))
C0 is functional Element of K6( the carrier of (TOP-REAL 2))
f is functional Element of K6( the carrier of (TOP-REAL 2))
g is V11() real ext-real Element of the carrier of I[01]
h is V11() real ext-real Element of the carrier of I[01]
p1 . g is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 . h is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 . g is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 . h is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dom p2 is V142() V143() V144() Element of K6( the carrier of I[01])
p2 (#) (Sq_Circ ") is Relation-like Function-like set
p1 (#) (Sq_Circ ") is Relation-like Function-like set
f2 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
dom f2 is V142() V143() V144() Element of K6( the carrier of I[01])
g2 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
dom g2 is V142() V143() V144() Element of K6( the carrier of I[01])
g2 . g is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(g2 . g) `1 is V11() real ext-real Element of REAL
g2 . h is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(g2 . h) `1 is V11() real ext-real Element of REAL
f2 . g is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(f2 . g) `2 is V11() real ext-real Element of REAL
f2 . h is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(f2 . h) `2 is V11() real ext-real Element of REAL
I is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
I `1 is V11() real ext-real Element of REAL
I `2 is V11() real ext-real Element of REAL
(I `2) / (I `1) is V11() real ext-real Element of REAL
((I `2) / (I `1)) ^2 is V11() real ext-real Element of REAL
K37(((I `2) / (I `1)),((I `2) / (I `1))) is V11() real ext-real set
1 + (((I `2) / (I `1)) ^2) is V11() real ext-real Element of REAL
sqrt (1 + (((I `2) / (I `1)) ^2)) is V11() real ext-real Element of REAL
(I `1) / (sqrt (1 + (((I `2) / (I `1)) ^2))) is V11() real ext-real Element of REAL
(I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2))) is V11() real ext-real Element of REAL
|[((I `1) / (sqrt (1 + (((I `2) / (I `1)) ^2)))),((I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2))))]| is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|[((I `1) / (sqrt (1 + (((I `2) / (I `1)) ^2)))),((I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2))))]| `1 is V11() real ext-real Element of REAL
O is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
O `1 is V11() real ext-real Element of REAL
O `2 is V11() real ext-real Element of REAL
(O `2) / (O `1) is V11() real ext-real Element of REAL
((O `2) / (O `1)) ^2 is V11() real ext-real Element of REAL
K37(((O `2) / (O `1)),((O `2) / (O `1))) is V11() real ext-real set
1 + (((O `2) / (O `1)) ^2) is V11() real ext-real Element of REAL
sqrt (1 + (((O `2) / (O `1)) ^2)) is V11() real ext-real Element of REAL
(O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2))) is V11() real ext-real Element of REAL
(O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2))) is V11() real ext-real Element of REAL
|[((O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2)))),((O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2))))]| is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|[((O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2)))),((O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2))))]| `1 is V11() real ext-real Element of REAL
KYP is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|.KYP.| is V11() real ext-real non negative Element of REAL
KYP `2 is V11() real ext-real Element of REAL
KYP `1 is V11() real ext-real Element of REAL
- (KYP `1) is V11() real ext-real Element of REAL
(Sq_Circ ") . (p1 . h) is set
Sq_Circ . O is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(Sq_Circ ") . KYP is set
(KYP `2) / (KYP `1) is V11() real ext-real Element of REAL
((KYP `2) / (KYP `1)) ^2 is V11() real ext-real Element of REAL
K37(((KYP `2) / (KYP `1)),((KYP `2) / (KYP `1))) is V11() real ext-real set
1 + (((KYP `2) / (KYP `1)) ^2) is V11() real ext-real Element of REAL
sqrt (1 + (((KYP `2) / (KYP `1)) ^2)) is V11() real ext-real Element of REAL
(KYP `1) * (sqrt (1 + (((KYP `2) / (KYP `1)) ^2))) is V11() real ext-real Element of REAL
(KYP `2) * (sqrt (1 + (((KYP `2) / (KYP `1)) ^2))) is V11() real ext-real Element of REAL
|[((KYP `1) * (sqrt (1 + (((KYP `2) / (KYP `1)) ^2)))),((KYP `2) * (sqrt (1 + (((KYP `2) / (KYP `1)) ^2))))]| is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(- (KYP `1)) * (sqrt (1 + (((KYP `2) / (KYP `1)) ^2))) is V11() real ext-real Element of REAL
- (O `1) is V11() real ext-real Element of REAL
- (KYP `2) is V11() real ext-real Element of REAL
- (- (KYP `1)) is V11() real ext-real Element of REAL
- (- (KYP `2)) is V11() real ext-real Element of REAL
- 0 is empty V11() real ext-real non positive non negative Function-like functional V142() V143() V144() V145() V146() V147() V148() V201() V204() Element of REAL
|[((O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2)))),((O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2))))]| `2 is V11() real ext-real Element of REAL
|.KYP.| ^2 is V11() real ext-real Element of REAL
K37(|.KYP.|,|.KYP.|) is V11() real ext-real non negative set
((O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2)))) ^2 is V11() real ext-real Element of REAL
K37(((O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2)))),((O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2))))) is V11() real ext-real set
((O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2)))) ^2 is V11() real ext-real Element of REAL
K37(((O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2)))),((O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2))))) is V11() real ext-real set
(((O `1) / (sqrt (1 + (((O `2) / (O `1)) ^2)))) ^2) + (((O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2)))) ^2) is V11() real ext-real Element of REAL
(O `1) ^2 is V11() real ext-real Element of REAL
K37((O `1),(O `1)) is V11() real ext-real set
(sqrt (1 + (((O `2) / (O `1)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt (1 + (((O `2) / (O `1)) ^2))),(sqrt (1 + (((O `2) / (O `1)) ^2)))) is V11() real ext-real set
((O `1) ^2) / ((sqrt (1 + (((O `2) / (O `1)) ^2))) ^2) is V11() real ext-real Element of REAL
(((O `1) ^2) / ((sqrt (1 + (((O `2) / (O `1)) ^2))) ^2)) + (((O `2) / (sqrt (1 + (((O `2) / (O `1)) ^2)))) ^2) is V11() real ext-real Element of REAL
(O `2) ^2 is V11() real ext-real Element of REAL
K37((O `2),(O `2)) is V11() real ext-real set
((O `2) ^2) / ((sqrt (1 + (((O `2) / (O `1)) ^2))) ^2) is V11() real ext-real Element of REAL
(((O `1) ^2) / ((sqrt (1 + (((O `2) / (O `1)) ^2))) ^2)) + (((O `2) ^2) / ((sqrt (1 + (((O `2) / (O `1)) ^2))) ^2)) is V11() real ext-real Element of REAL
((O `1) ^2) / (1 + (((O `2) / (O `1)) ^2)) is V11() real ext-real Element of REAL
(((O `1) ^2) / (1 + (((O `2) / (O `1)) ^2))) + (((O `2) ^2) / ((sqrt (1 + (((O `2) / (O `1)) ^2))) ^2)) is V11() real ext-real Element of REAL
((O `2) ^2) / (1 + (((O `2) / (O `1)) ^2)) is V11() real ext-real Element of REAL
(((O `1) ^2) / (1 + (((O `2) / (O `1)) ^2))) + (((O `2) ^2) / (1 + (((O `2) / (O `1)) ^2))) is V11() real ext-real Element of REAL
((O `1) ^2) + ((O `2) ^2) is V11() real ext-real Element of REAL
(((O `1) ^2) + ((O `2) ^2)) / (1 + (((O `2) / (O `1)) ^2)) is V11() real ext-real Element of REAL
((((O `1) ^2) + ((O `2) ^2)) / (1 + (((O `2) / (O `1)) ^2))) * (1 + (((O `2) / (O `1)) ^2)) is V11() real ext-real Element of REAL
1 * (1 + (((O `2) / (O `1)) ^2)) is V11() real ext-real Element of REAL
(((O `1) ^2) + ((O `2) ^2)) - 1 is V11() real ext-real Element of REAL
((O `2) ^2) / ((O `1) ^2) is V11() real ext-real Element of REAL
((((O `1) ^2) + ((O `2) ^2)) - 1) * ((O `1) ^2) is V11() real ext-real Element of REAL
((O `1) ^2) - 1 is V11() real ext-real Element of REAL
(((O `1) ^2) - 1) * (((O `1) ^2) + ((O `2) ^2)) is V11() real ext-real Element of REAL
(O `1) - 1 is V11() real ext-real Element of REAL
(O `1) + 1 is V11() real ext-real Element of REAL
((O `1) - 1) * ((O `1) + 1) is V11() real ext-real Element of REAL
h1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
h1 `1 is V11() real ext-real Element of REAL
h1 `2 is V11() real ext-real Element of REAL
(h1 `1) / (h1 `2) is V11() real ext-real Element of REAL
((h1 `1) / (h1 `2)) ^2 is V11() real ext-real Element of REAL
K37(((h1 `1) / (h1 `2)),((h1 `1) / (h1 `2))) is V11() real ext-real set
1 + (((h1 `1) / (h1 `2)) ^2) is V11() real ext-real Element of REAL
sqrt (1 + (((h1 `1) / (h1 `2)) ^2)) is V11() real ext-real Element of REAL
(h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) is V11() real ext-real Element of REAL
(h1 `2) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) is V11() real ext-real Element of REAL
|[((h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))),((h1 `2) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2))))]| is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|[((h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))),((h1 `2) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2))))]| `2 is V11() real ext-real Element of REAL
KYN is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|.KYN.| is V11() real ext-real non negative Element of REAL
KYN `1 is V11() real ext-real Element of REAL
KYN `2 is V11() real ext-real Element of REAL
- (KYN `1) is V11() real ext-real Element of REAL
(KYN `2) / (KYN `1) is V11() real ext-real Element of REAL
((KYN `2) / (KYN `1)) ^2 is V11() real ext-real Element of REAL
K37(((KYN `2) / (KYN `1)),((KYN `2) / (KYN `1))) is V11() real ext-real set
1 + (((KYN `2) / (KYN `1)) ^2) is V11() real ext-real Element of REAL
sqrt (1 + (((KYN `2) / (KYN `1)) ^2)) is V11() real ext-real Element of REAL
(Sq_Circ ") . (p1 . g) is set
Sq_Circ . I is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(Sq_Circ ") . KYN is set
(KYN `1) * (sqrt (1 + (((KYN `2) / (KYN `1)) ^2))) is V11() real ext-real Element of REAL
(KYN `2) * (sqrt (1 + (((KYN `2) / (KYN `1)) ^2))) is V11() real ext-real Element of REAL
|[((KYN `1) * (sqrt (1 + (((KYN `2) / (KYN `1)) ^2)))),((KYN `2) * (sqrt (1 + (((KYN `2) / (KYN `1)) ^2))))]| is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(- (KYN `1)) * (sqrt (1 + (((KYN `2) / (KYN `1)) ^2))) is V11() real ext-real Element of REAL
- (I `1) is V11() real ext-real Element of REAL
- (- (KYN `1)) is V11() real ext-real Element of REAL
- (KYN `2) is V11() real ext-real Element of REAL
- (- (KYN `2)) is V11() real ext-real Element of REAL
|[((I `1) / (sqrt (1 + (((I `2) / (I `1)) ^2)))),((I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2))))]| `2 is V11() real ext-real Element of REAL
|.KYN.| ^2 is V11() real ext-real Element of REAL
K37(|.KYN.|,|.KYN.|) is V11() real ext-real non negative set
((I `1) / (sqrt (1 + (((I `2) / (I `1)) ^2)))) ^2 is V11() real ext-real Element of REAL
K37(((I `1) / (sqrt (1 + (((I `2) / (I `1)) ^2)))),((I `1) / (sqrt (1 + (((I `2) / (I `1)) ^2))))) is V11() real ext-real set
((I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2)))) ^2 is V11() real ext-real Element of REAL
K37(((I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2)))),((I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2))))) is V11() real ext-real set
(((I `1) / (sqrt (1 + (((I `2) / (I `1)) ^2)))) ^2) + (((I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2)))) ^2) is V11() real ext-real Element of REAL
(I `1) ^2 is V11() real ext-real Element of REAL
K37((I `1),(I `1)) is V11() real ext-real set
(sqrt (1 + (((I `2) / (I `1)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt (1 + (((I `2) / (I `1)) ^2))),(sqrt (1 + (((I `2) / (I `1)) ^2)))) is V11() real ext-real set
((I `1) ^2) / ((sqrt (1 + (((I `2) / (I `1)) ^2))) ^2) is V11() real ext-real Element of REAL
(((I `1) ^2) / ((sqrt (1 + (((I `2) / (I `1)) ^2))) ^2)) + (((I `2) / (sqrt (1 + (((I `2) / (I `1)) ^2)))) ^2) is V11() real ext-real Element of REAL
(I `2) ^2 is V11() real ext-real Element of REAL
K37((I `2),(I `2)) is V11() real ext-real set
((I `2) ^2) / ((sqrt (1 + (((I `2) / (I `1)) ^2))) ^2) is V11() real ext-real Element of REAL
(((I `1) ^2) / ((sqrt (1 + (((I `2) / (I `1)) ^2))) ^2)) + (((I `2) ^2) / ((sqrt (1 + (((I `2) / (I `1)) ^2))) ^2)) is V11() real ext-real Element of REAL
((I `1) ^2) / (1 + (((I `2) / (I `1)) ^2)) is V11() real ext-real Element of REAL
(((I `1) ^2) / (1 + (((I `2) / (I `1)) ^2))) + (((I `2) ^2) / ((sqrt (1 + (((I `2) / (I `1)) ^2))) ^2)) is V11() real ext-real Element of REAL
((I `2) ^2) / (1 + (((I `2) / (I `1)) ^2)) is V11() real ext-real Element of REAL
(((I `1) ^2) / (1 + (((I `2) / (I `1)) ^2))) + (((I `2) ^2) / (1 + (((I `2) / (I `1)) ^2))) is V11() real ext-real Element of REAL
((I `1) ^2) + ((I `2) ^2) is V11() real ext-real Element of REAL
(((I `1) ^2) + ((I `2) ^2)) / (1 + (((I `2) / (I `1)) ^2)) is V11() real ext-real Element of REAL
((((I `1) ^2) + ((I `2) ^2)) / (1 + (((I `2) / (I `1)) ^2))) * (1 + (((I `2) / (I `1)) ^2)) is V11() real ext-real Element of REAL
1 * (1 + (((I `2) / (I `1)) ^2)) is V11() real ext-real Element of REAL
(((I `1) ^2) + ((I `2) ^2)) - 1 is V11() real ext-real Element of REAL
((I `2) ^2) / ((I `1) ^2) is V11() real ext-real Element of REAL
((((I `1) ^2) + ((I `2) ^2)) - 1) * ((I `1) ^2) is V11() real ext-real Element of REAL
((I `1) ^2) - 1 is V11() real ext-real Element of REAL
(((I `1) ^2) - 1) * (((I `1) ^2) + ((I `2) ^2)) is V11() real ext-real Element of REAL
KXN is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
KXN `1 is V11() real ext-real Element of REAL
KXN `2 is V11() real ext-real Element of REAL
(KXN `1) / (KXN `2) is V11() real ext-real Element of REAL
((KXN `1) / (KXN `2)) ^2 is V11() real ext-real Element of REAL
K37(((KXN `1) / (KXN `2)),((KXN `1) / (KXN `2))) is V11() real ext-real set
1 + (((KXN `1) / (KXN `2)) ^2) is V11() real ext-real Element of REAL
sqrt (1 + (((KXN `1) / (KXN `2)) ^2)) is V11() real ext-real Element of REAL
(KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) is V11() real ext-real Element of REAL
(KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) is V11() 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) V76() V134() Element of the carrier of (TOP-REAL 2)
|[((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))),((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))))]| `2 is V11() real ext-real Element of REAL
x2 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|.x2.| is V11() real ext-real non negative Element of REAL
x2 `1 is V11() real ext-real Element of REAL
x2 `2 is V11() real ext-real Element of REAL
- (x2 `1) is V11() real ext-real Element of REAL
(x2 `1) / (x2 `2) is V11() real ext-real Element of REAL
((x2 `1) / (x2 `2)) ^2 is V11() real ext-real Element of REAL
K37(((x2 `1) / (x2 `2)),((x2 `1) / (x2 `2))) is V11() real ext-real set
1 + (((x2 `1) / (x2 `2)) ^2) is V11() real ext-real Element of REAL
sqrt (1 + (((x2 `1) / (x2 `2)) ^2)) is V11() real ext-real Element of REAL
- (x2 `2) is V11() real ext-real Element of REAL
- (- (x2 `1)) is V11() real ext-real Element of REAL
(- (x2 `2)) * (sqrt (1 + (((x2 `1) / (x2 `2)) ^2))) is V11() real ext-real Element of REAL
(x2 `1) * (sqrt (1 + (((x2 `1) / (x2 `2)) ^2))) is V11() real ext-real Element of REAL
- (KXN `2) is V11() real ext-real Element of REAL
(Sq_Circ ") . (p2 . h) is set
Sq_Circ . KXN is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(Sq_Circ ") . x2 is set
(x2 `2) * (sqrt (1 + (((x2 `1) / (x2 `2)) ^2))) is V11() real ext-real Element of REAL
|[((x2 `1) * (sqrt (1 + (((x2 `1) / (x2 `2)) ^2)))),((x2 `2) * (sqrt (1 + (((x2 `1) / (x2 `2)) ^2))))]| is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|[((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))),((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))))]| `1 is V11() real ext-real Element of REAL
|.x2.| ^2 is V11() real ext-real Element of REAL
K37(|.x2.|,|.x2.|) is V11() real ext-real non negative set
((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))) ^2 is V11() real ext-real Element of REAL
K37(((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))),((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))))) is V11() real ext-real set
((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))) ^2 is V11() real ext-real Element of REAL
K37(((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))),((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2))))) is V11() real ext-real set
(((KXN `2) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))) ^2) + (((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))) ^2) is V11() real ext-real Element of REAL
(KXN `2) ^2 is V11() real ext-real Element of REAL
K37((KXN `2),(KXN `2)) is V11() real ext-real set
(sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt (1 + (((KXN `1) / (KXN `2)) ^2))),(sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))) is V11() real ext-real set
((KXN `2) ^2) / ((sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) ^2) is V11() real ext-real Element of REAL
(((KXN `2) ^2) / ((sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) ^2)) + (((KXN `1) / (sqrt (1 + (((KXN `1) / (KXN `2)) ^2)))) ^2) is V11() real ext-real Element of REAL
(KXN `1) ^2 is V11() real ext-real Element of REAL
K37((KXN `1),(KXN `1)) is V11() real ext-real set
((KXN `1) ^2) / ((sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) ^2) is V11() real ext-real Element of REAL
(((KXN `2) ^2) / ((sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) ^2)) + (((KXN `1) ^2) / ((sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) ^2)) is V11() real ext-real Element of REAL
((KXN `2) ^2) / (1 + (((KXN `1) / (KXN `2)) ^2)) is V11() real ext-real Element of REAL
(((KXN `2) ^2) / (1 + (((KXN `1) / (KXN `2)) ^2))) + (((KXN `1) ^2) / ((sqrt (1 + (((KXN `1) / (KXN `2)) ^2))) ^2)) is V11() real ext-real Element of REAL
((KXN `1) ^2) / (1 + (((KXN `1) / (KXN `2)) ^2)) is V11() real ext-real Element of REAL
(((KXN `2) ^2) / (1 + (((KXN `1) / (KXN `2)) ^2))) + (((KXN `1) ^2) / (1 + (((KXN `1) / (KXN `2)) ^2))) is V11() real ext-real Element of REAL
((KXN `2) ^2) + ((KXN `1) ^2) is V11() real ext-real Element of REAL
(((KXN `2) ^2) + ((KXN `1) ^2)) / (1 + (((KXN `1) / (KXN `2)) ^2)) is V11() real ext-real Element of REAL
((((KXN `2) ^2) + ((KXN `1) ^2)) / (1 + (((KXN `1) / (KXN `2)) ^2))) * (1 + (((KXN `1) / (KXN `2)) ^2)) is V11() real ext-real Element of REAL
1 * (1 + (((KXN `1) / (KXN `2)) ^2)) is V11() real ext-real Element of REAL
(((KXN `2) ^2) + ((KXN `1) ^2)) - 1 is V11() real ext-real Element of REAL
((KXN `1) ^2) / ((KXN `2) ^2) is V11() real ext-real Element of REAL
((((KXN `2) ^2) + ((KXN `1) ^2)) - 1) * ((KXN `2) ^2) is V11() real ext-real Element of REAL
((KXN `2) ^2) - 1 is V11() real ext-real Element of REAL
(((KXN `2) ^2) - 1) * (((KXN `2) ^2) + ((KXN `1) ^2)) is V11() real ext-real Element of REAL
(KXN `2) - 1 is V11() real ext-real Element of REAL
(KXN `2) + 1 is V11() real ext-real Element of REAL
((KXN `2) - 1) * ((KXN `2) + 1) is V11() real ext-real Element of REAL
z3 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|.z3.| is V11() real ext-real non negative Element of REAL
z3 `2 is V11() real ext-real Element of REAL
z3 `1 is V11() real ext-real Element of REAL
- (z3 `1) is V11() real ext-real Element of REAL
(Sq_Circ ") . (p2 . g) is set
Sq_Circ . h1 is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
- (- (z3 `1)) is V11() real ext-real Element of REAL
- (z3 `2) is V11() real ext-real Element of REAL
(Sq_Circ ") . z3 is set
(z3 `1) / (z3 `2) is V11() real ext-real Element of REAL
((z3 `1) / (z3 `2)) ^2 is V11() real ext-real Element of REAL
K37(((z3 `1) / (z3 `2)),((z3 `1) / (z3 `2))) is V11() real ext-real set
1 + (((z3 `1) / (z3 `2)) ^2) is V11() real ext-real Element of REAL
sqrt (1 + (((z3 `1) / (z3 `2)) ^2)) is V11() real ext-real Element of REAL
(z3 `1) * (sqrt (1 + (((z3 `1) / (z3 `2)) ^2))) is V11() real ext-real Element of REAL
(z3 `2) * (sqrt (1 + (((z3 `1) / (z3 `2)) ^2))) is V11() real ext-real Element of REAL
|[((z3 `1) * (sqrt (1 + (((z3 `1) / (z3 `2)) ^2)))),((z3 `2) * (sqrt (1 + (((z3 `1) / (z3 `2)) ^2))))]| is Relation-like Function-like V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(- (z3 `2)) * (sqrt (1 + (((z3 `1) / (z3 `2)) ^2))) is V11() real ext-real Element of REAL
- (h1 `2) is V11() real ext-real Element of REAL
|[((h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))),((h1 `2) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2))))]| `1 is V11() real ext-real Element of REAL
|.z3.| ^2 is V11() real ext-real Element of REAL
K37(|.z3.|,|.z3.|) is V11() real ext-real non negative set
((h1 `2) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))) ^2 is V11() real ext-real Element of REAL
K37(((h1 `2) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))),((h1 `2) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2))))) is V11() real ext-real set
((h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))) ^2 is V11() real ext-real Element of REAL
K37(((h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))),((h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2))))) is V11() real ext-real set
(((h1 `2) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))) ^2) + (((h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))) ^2) is V11() real ext-real Element of REAL
(h1 `2) ^2 is V11() real ext-real Element of REAL
K37((h1 `2),(h1 `2)) is V11() real ext-real set
(sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) ^2 is V11() real ext-real Element of REAL
K37((sqrt (1 + (((h1 `1) / (h1 `2)) ^2))),(sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))) is V11() real ext-real set
((h1 `2) ^2) / ((sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) ^2) is V11() real ext-real Element of REAL
(((h1 `2) ^2) / ((sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) ^2)) + (((h1 `1) / (sqrt (1 + (((h1 `1) / (h1 `2)) ^2)))) ^2) is V11() real ext-real Element of REAL
(h1 `1) ^2 is V11() real ext-real Element of REAL
K37((h1 `1),(h1 `1)) is V11() real ext-real set
((h1 `1) ^2) / ((sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) ^2) is V11() real ext-real Element of REAL
(((h1 `2) ^2) / ((sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) ^2)) + (((h1 `1) ^2) / ((sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) ^2)) is V11() real ext-real Element of REAL
((h1 `2) ^2) / (1 + (((h1 `1) / (h1 `2)) ^2)) is V11() real ext-real Element of REAL
(((h1 `2) ^2) / (1 + (((h1 `1) / (h1 `2)) ^2))) + (((h1 `1) ^2) / ((sqrt (1 + (((h1 `1) / (h1 `2)) ^2))) ^2)) is V11() real ext-real Element of REAL
((h1 `1) ^2) / (1 + (((h1 `1) / (h1 `2)) ^2)) is V11() real ext-real Element of REAL
(((h1 `2) ^2) / (1 + (((h1 `1) / (h1 `2)) ^2))) + (((h1 `1) ^2) / (1 + (((h1 `1) / (h1 `2))