let cn be Real; :: thesis: for K1 being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K1),R^1 st - 1 < cn & ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `2 <= 0 & (q `1) / |.q.| <= cn & q <> 0. (TOP-REAL 2) ) ) holds
f is continuous
let K1 be non empty Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K1),R^1 st - 1 < cn & ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `2 <= 0 & (q `1) / |.q.| <= cn & q <> 0. (TOP-REAL 2) ) ) holds
f is continuous
let f be Function of ((TOP-REAL 2) | K1),R^1; :: thesis: ( - 1 < cn & ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `2 <= 0 & (q `1) / |.q.| <= cn & q <> 0. (TOP-REAL 2) ) ) implies f is continuous )
reconsider g1 = (2 NormF) | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm5;
set a = cn;
set b = 1 + cn;
reconsider g2 = proj1 | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm2;
assume that
A1: - 1 < cn and
A2: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)))) and
A3: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `2 <= 0 & (q `1) / |.q.| <= cn & q <> 0. (TOP-REAL 2) ) ; :: thesis: f is continuous
A4: 1 + cn > 0 by A1, XREAL_1:148;
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q <> 0. (TOP-REAL 2) by A3;
then for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0 by Lm6;
then consider g3 being Function of ((TOP-REAL 2) | K1),R^1 such that
A5: for q being Point of ((TOP-REAL 2) | K1)
for r1, r2 being Real st g2 . q = r1 & g1 . q = r2 holds
g3 . q = r2 * (- (sqrt |.(1 - ((((r1 / r2) - cn) / (1 + cn)) ^2)).|)) and
A6: g3 is continuous by A4, Th9;
A7: dom g3 = the carrier of ((TOP-REAL 2) | K1) by FUNCT_2:def 1;
then A8: dom f = dom g3 by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = g3 . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = g3 . x )
assume A9: x in dom f ; :: thesis: f . x = g3 . x
then x in K1 by A7, A8, PRE_TOPC:8;
then reconsider r = x as Point of (TOP-REAL 2) ;
reconsider s = x as Point of ((TOP-REAL 2) | K1) by A9;
A10: (1 + cn) ^2 > 0 by A4, SQUARE_1:12;
A11: |.r.| <> 0 by A3, A9, TOPRNS_1:24;
|.r.| ^2 = ((r `1) ^2) + ((r `2) ^2) by JGRAPH_3:1;
then A12: ((r `1) - |.r.|) * ((r `1) + |.r.|) = - ((r `2) ^2) ;
(r `2) ^2 >= 0 by XREAL_1:63;
then - |.r.| <= r `1 by A12, XREAL_1:93;
then (r `1) / |.r.| >= (- |.r.|) / |.r.| by XREAL_1:72;
then (r `1) / |.r.| >= - 1 by A11, XCMPLX_1:197;
then ((r `1) / |.r.|) - cn >= (- 1) - cn by XREAL_1:9;
then A13: ((r `1) / |.r.|) - cn >= - (1 + cn) ;
cn - ((r `1) / |.r.|) >= 0 by A3, A9, XREAL_1:48;
then - (cn - ((r `1) / |.r.|)) <= - 0 ;
then (((r `1) / |.r.|) - cn) ^2 <= (1 + cn) ^2 by A4, A13, SQUARE_1:49;
then ((((r `1) / |.r.|) - cn) ^2) / ((1 + cn) ^2) <= ((1 + cn) ^2) / ((1 + cn) ^2) by A4, XREAL_1:72;
then ((((r `1) / |.r.|) - cn) ^2) / ((1 + cn) ^2) <= 1 by A10, XCMPLX_1:60;
then ((((r `1) / |.r.|) - cn) / (1 + cn)) ^2 <= 1 by XCMPLX_1:76;
then 1 - (((((r `1) / |.r.|) - cn) / (1 + cn)) ^2) >= 0 by XREAL_1:48;
then |.(1 - (((((r `1) / |.r.|) - cn) / (1 + cn)) ^2)).| = 1 - (((((r `1) / |.r.|) - cn) / (1 + cn)) ^2) by ABSVALUE:def 1;
then A14: f . r = |.r.| * (- (sqrt |.(1 - (((((r `1) / |.r.|) - cn) / (1 + cn)) ^2)).|)) by A2, A9;
A15: ( proj1 . r = r `1 & (2 NormF) . r = |.r.| ) by Def1, PSCOMP_1:def 5;
( g2 . s = proj1 . s & g1 . s = (2 NormF) . s ) by Lm2, Lm5;
hence f . x = g3 . x by A5, A14, A15; :: thesis: verum

end;

hence f is continuous by A6, A8, FUNCT_1:2; :: thesis: verum