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

let f be Function of (() | K0),(() | B0); :: thesis: ( f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. () ) } implies f is continuous )
assume A1: ( f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. () ) } ) ; :: thesis: f is continuous
then 1.REAL 2 in K0 by ;
then reconsider K1 = K0 as non empty Subset of () ;
( dom (proj2 * (Sq_Circ | K1)) = the carrier of (() | K1) & rng (proj2 * (Sq_Circ | K1)) c= the carrier of R^1 ) by ;
then reconsider g1 = proj2 * (Sq_Circ | K1) as Function of (() | K1),R^1 by FUNCT_2:2;
for p being Point of () st p in the carrier of (() | K1) holds
g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))
proof
let p be Point of (); :: thesis: ( p in the carrier of (() | K1) implies g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) )
A2: dom (Sq_Circ | K1) = () /\ K1 by RELAT_1:61
.= the carrier of () /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28 ;
A3: the carrier of (() | K1) = K1 by PRE_TOPC:8;
assume A4: p in the carrier of (() | K1) ; :: thesis: g1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))
then ex p3 being Point of () st
( p = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. () ) 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 ;
then g1 . p = proj2 . |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by
.= |[((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 (() | K1),R^1 such that
A6: for p being Point of () st p in the carrier of (() | K1) holds
f1 . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ;
( dom (proj1 * (Sq_Circ | K1)) = the carrier of (() | K1) & rng (proj1 * (Sq_Circ | K1)) c= the carrier of R^1 ) by ;
then reconsider g2 = proj1 * (Sq_Circ | K1) as Function of (() | K1),R^1 by FUNCT_2:2;
for p being Point of () st p in the carrier of (() | K1) holds
g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))
proof
let p be Point of (); :: thesis: ( p in the carrier of (() | K1) implies g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) )
A7: dom (Sq_Circ | K1) = () /\ K1 by RELAT_1:61
.= the carrier of () /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28 ;
A8: the carrier of (() | K1) = K1 by PRE_TOPC:8;
assume A9: p in the carrier of (() | K1) ; :: thesis: g2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))
then ex p3 being Point of () st
( p = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. () ) 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 ;
then g2 . p = proj1 . |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by
.= |[((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 (() | K1),R^1 such that
A11: for p being Point of () st p in the carrier of (() | K1) holds
f2 . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ;
A12: for q being Point of () st q in the carrier of (() | K1) holds
q `2 <> 0
proof
let q be Point of (); :: thesis: ( q in the carrier of (() | K1) implies q `2 <> 0 )
A13: the carrier of (() | K1) = K1 by PRE_TOPC:8;
assume q in the carrier of (() | K1) ; :: thesis:
then A14: ex p3 being Point of () st
( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. () ) by ;
now :: thesis: not q `2 = 0 end;
hence q `2 <> 0 ; :: thesis: verum
end;
then A16: f1 is continuous by ;
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]|
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 () st
( |[x,y]| = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2) ) ) & p3 <> 0. () ) by ;
A21: the carrier of (() | K1) = K1 by PRE_TOPC:8;
then A22: f1 . |[x,y]| = (|[x,y]| `2) / (sqrt (1 + (((|[x,y]| `1) / (|[x,y]| `2)) ^2))) by ;
(Sq_Circ | K0) . |[x,y]| = Sq_Circ . |[x,y]| by
.= |[((|[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
.= |[s,r]| by A11, A18, A19, A21, A22 ;
hence f . |[x,y]| = |[s,r]| by A1; :: thesis: verum
end;
f2 is continuous by ;
hence f is continuous by ; :: thesis: verum