let K0, B0 be Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Sq_Circ | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); :: thesis: ( f = Sq_Circ | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } implies f is continuous )

assume A1: ( f = Sq_Circ | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: f is continuous

then 1.REAL 2 in K0 by Lm14, Lm15;

then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;

( dom (proj2 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1) & rng (proj2 * (Sq_Circ | K1)) c= the carrier of R^1 ) by Lm11, TOPMETR:17;

then reconsider g1 = proj2 * (Sq_Circ | K1) as Function of ((TOP-REAL 2) | K1),R^1 by FUNCT_2:2;

for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))

A6: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ;

( dom (proj1 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1) & rng (proj1 * (Sq_Circ | K1)) c= the carrier of R^1 ) by Lm12, TOPMETR:17;

then reconsider g2 = proj1 * (Sq_Circ | K1) as Function of ((TOP-REAL 2) | K1),R^1 by FUNCT_2:2;

for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))

A11: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ;

A12: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0

hence f is continuous by A1, A16, A17, Lm13, JGRAPH_2:35; :: thesis: verum

f is continuous

let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); :: thesis: ( f = Sq_Circ | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } implies f is continuous )

assume A1: ( f = Sq_Circ | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: f is continuous

then 1.REAL 2 in K0 by Lm14, Lm15;

then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;

( dom (proj2 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1) & rng (proj2 * (Sq_Circ | K1)) c= the carrier of R^1 ) by Lm11, TOPMETR:17;

then reconsider g1 = proj2 * (Sq_Circ | K1) as Function of ((TOP-REAL 2) | K1),R^1 by FUNCT_2:2;

for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))

proof

then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) )

A2: dom (Sq_Circ | K1) = (dom Sq_Circ) /\ K1 by RELAT_1:61

.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1

.= K1 by XBOOLE_1:28 ;

A3: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

assume A4: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))

then ex p3 being Point of (TOP-REAL 2) st

( p = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A3;

then A5: Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by Th4;

(Sq_Circ | K1) . p = Sq_Circ . p by A4, A3, FUNCT_1:49;

then g1 . p = proj2 . |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by A4, A2, A3, A5, FUNCT_1:13

.= |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 by PSCOMP_1:def 6

.= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by EUCLID:52 ;

hence g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ; :: thesis: verum

end;A2: dom (Sq_Circ | K1) = (dom Sq_Circ) /\ K1 by RELAT_1:61

.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1

.= K1 by XBOOLE_1:28 ;

A3: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

assume A4: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))

then ex p3 being Point of (TOP-REAL 2) st

( p = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A3;

then A5: Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by Th4;

(Sq_Circ | K1) . p = Sq_Circ . p by A4, A3, FUNCT_1:49;

then g1 . p = proj2 . |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by A4, A2, A3, A5, FUNCT_1:13

.= |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 by PSCOMP_1:def 6

.= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by EUCLID:52 ;

hence g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ; :: thesis: verum

A6: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ;

( dom (proj1 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1) & rng (proj1 * (Sq_Circ | K1)) c= the carrier of R^1 ) by Lm12, TOPMETR:17;

then reconsider g2 = proj1 * (Sq_Circ | K1) as Function of ((TOP-REAL 2) | K1),R^1 by FUNCT_2:2;

for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))

proof

then consider f2 being Function of ((TOP-REAL 2) | K1),R^1 such that
let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) )

A7: dom (Sq_Circ | K1) = (dom Sq_Circ) /\ K1 by RELAT_1:61

.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1

.= K1 by XBOOLE_1:28 ;

A8: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

assume A9: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))

then ex p3 being Point of (TOP-REAL 2) st

( p = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A8;

then A10: Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by Th4;

(Sq_Circ | K1) . p = Sq_Circ . p by A9, A8, FUNCT_1:49;

then g2 . p = proj1 . |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by A9, A7, A8, A10, FUNCT_1:13

.= |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 by PSCOMP_1:def 5

.= (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by EUCLID:52 ;

hence g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ; :: thesis: verum

end;A7: dom (Sq_Circ | K1) = (dom Sq_Circ) /\ K1 by RELAT_1:61

.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1

.= K1 by XBOOLE_1:28 ;

A8: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

assume A9: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))

then ex p3 being Point of (TOP-REAL 2) st

( p = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A8;

then A10: Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by Th4;

(Sq_Circ | K1) . p = Sq_Circ . p by A9, A8, FUNCT_1:49;

then g2 . p = proj1 . |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by A9, A7, A8, A10, FUNCT_1:13

.= |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 by PSCOMP_1:def 5

.= (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by EUCLID:52 ;

hence g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ; :: thesis: verum

A11: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ;

A12: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0

proof

then A16:
f1 is continuous
by A6, Th13;
let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K1) implies q `2 <> 0 )

A13: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

assume q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: q `2 <> 0

then A14: ex p3 being Point of (TOP-REAL 2) st

( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A13;

end;A13: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

assume q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: q `2 <> 0

then A14: ex p3 being Point of (TOP-REAL 2) st

( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A13;

now :: thesis: not q `2 = 0

hence
q `2 <> 0
; :: thesis: verumassume A15:
q `2 = 0
; :: thesis: contradiction

then q `1 = 0 by A14;

hence contradiction by A14, A15, EUCLID:53, EUCLID:54; :: thesis: verum

end;then q `1 = 0 by A14;

hence contradiction by A14, A15, EUCLID:53, EUCLID:54; :: thesis: verum

A17: now :: thesis: for x, y, s, r being Real st |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| holds

f . |[x,y]| = |[s,r]|

f2 is continuous
by A12, A11, Th14;f . |[x,y]| = |[s,r]|

let x, y, s, r be Real; :: thesis: ( |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| implies f . |[x,y]| = |[s,r]| )

assume that

A18: |[x,y]| in K1 and

A19: ( s = f2 . |[x,y]| & r = f1 . |[x,y]| ) ; :: thesis: f . |[x,y]| = |[s,r]|

set p99 = |[x,y]|;

A20: ex p3 being Point of (TOP-REAL 2) st

( |[x,y]| = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A18;

A21: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

then A22: f1 . |[x,y]| = (|[x,y]| `2) / (sqrt (1 + (((|[x,y]| `1) / (|[x,y]| `2)) ^2))) by A6, A18;

(Sq_Circ | K0) . |[x,y]| = Sq_Circ . |[x,y]| by A18, FUNCT_1:49

.= |[((|[x,y]| `1) / (sqrt (1 + (((|[x,y]| `1) / (|[x,y]| `2)) ^2)))),((|[x,y]| `2) / (sqrt (1 + (((|[x,y]| `1) / (|[x,y]| `2)) ^2))))]| by A20, Th4

.= |[s,r]| by A11, A18, A19, A21, A22 ;

hence f . |[x,y]| = |[s,r]| by A1; :: thesis: verum

end;assume that

A18: |[x,y]| in K1 and

A19: ( s = f2 . |[x,y]| & r = f1 . |[x,y]| ) ; :: thesis: f . |[x,y]| = |[s,r]|

set p99 = |[x,y]|;

A20: ex p3 being Point of (TOP-REAL 2) st

( |[x,y]| = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A18;

A21: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

then A22: f1 . |[x,y]| = (|[x,y]| `2) / (sqrt (1 + (((|[x,y]| `1) / (|[x,y]| `2)) ^2))) by A6, A18;

(Sq_Circ | K0) . |[x,y]| = Sq_Circ . |[x,y]| by A18, FUNCT_1:49

.= |[((|[x,y]| `1) / (sqrt (1 + (((|[x,y]| `1) / (|[x,y]| `2)) ^2)))),((|[x,y]| `2) / (sqrt (1 + (((|[x,y]| `1) / (|[x,y]| `2)) ^2))))]| by A20, Th4

.= |[s,r]| by A11, A18, A19, A21, A22 ;

hence f . |[x,y]| = |[s,r]| by A1; :: thesis: verum

hence f is continuous by A1, A16, A17, Lm13, JGRAPH_2:35; :: thesis: verum