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:90
.= the carrier of (TOP-REAL 2) /\ K1 by Th39, 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:29;
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 Th40;
((Sq_Circ " ) | K1) . p = (Sq_Circ " ) . p by A4, A3, FUNCT_1:72;
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:23
.= |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| `2 by PSCOMP_1:def 29
.= (p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))) by EUCLID:56 ;
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:90
.= the carrier of (TOP-REAL 2) /\ K1 by Th39, 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:29;
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 Th40;
((Sq_Circ " ) | K1) . p = (Sq_Circ " ) . p by A9, A8, FUNCT_1:72;
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:23
.= |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| `1 by PSCOMP_1:def 28
.= (p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))) by EUCLID:56 ;
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:29;
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

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

end;

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

end;

then A16: f1 is continuous by A6, Th45;
A17: for x, y, s, r being real number 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 number ; :: 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:29;
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:72
.= |[((|[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, Th40
.= |[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, Th46;
hence f is continuous by A1, A16, A17, Lm13, JGRAPH_2:45; :: thesis: verum