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

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