:: JGRAPH_5 semantic presentation

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

{ b

Sq_Circ " is Relation-like Function-like set

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

{ b

{ b

{ b

{ b

{ b

- 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

{ b

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

{ b

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

{ b

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