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) ;
reconsider g1 = proj2 * ((Sq_Circ ") | K1) as Function of ((TOP-REAL 2) | K1),R^1 by Lm17;
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

A2: dom ((Sq_Circ ") | K1) = (dom (Sq_Circ ")) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by Th29, FUNCT_2:def 1
.= K1 by XBOOLE_1:28 ;
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))) )
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 Th30;
((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;

then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
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))) ;
reconsider g2 = proj1 * ((Sq_Circ ") | K1) as Function of ((TOP-REAL 2) | K1),R^1 by Lm18;
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

A7: dom ((Sq_Circ ") | K1) = (dom (Sq_Circ ")) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by Th29, FUNCT_2:def 1
.= K1 by XBOOLE_1:28 ;
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))) )
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 Th30;
((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;

then consider f2 being Function of ((TOP-REAL 2) | K1),R^1 such that
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

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;

now :: thesis: not q `2 = 0

assume A15: q `2 = 0 ; :: thesis: contradiction
then q `1 = 0 by A14;
hence contradiction by A14, A15, EUCLID:53, EUCLID:54; :: thesis: verum

end;

hence q `2 <> 0 ; :: thesis: verum

end;

then A16: f1 is continuous by A6, Th35;
A17: 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]|

proof

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, Th30
.= |[s,r]| by A11, A18, A19, A21, A22 ;
hence f . |[x,y]| = |[s,r]| by A1; :: thesis: verum

end;

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