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 & cn < 1 & ( 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 & cn < 1 & ( 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 & cn < 1 & ( 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 )
assume A1: ( - 1 < cn & cn < 1 & ( 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) ) ) ) ; :: thesis: f is continuous
set a = cn;
set b = 1 - cn;
A2: 1 - cn > 0 by A1, XREAL_1:151;
reconsider g2 = proj1 | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm2;
reconsider g1 = (2 NormF ) | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm5;
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 A1;
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
A3: ( ( for q being Point of ((TOP-REAL 2) | K1)
for r1, r2 being real number st g2 . q = r1 & g1 . q = r2 holds
g3 . q = r2 * (sqrt (abs (1 - ((((r1 / r2) - cn) / (1 - cn)) ^2 )))) ) & g3 is continuous ) by A2, Th15;
A4: dom g3 = the carrier of ((TOP-REAL 2) | K1) by FUNCT_2:def 1;
then A5: dom f = dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds
f . x = g3 . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x = g3 . x )
assume A6: x in dom f ; :: thesis: f . x = g3 . x
then x in K1 by A4, A5, PRE_TOPC:29;
then reconsider r = x as Point of (TOP-REAL 2) ;
reconsider s = x as Point of ((TOP-REAL 2) | K1) by A6;

A7: now

assume |.r.| = 0 ; :: thesis: contradiction
then r = 0. (TOP-REAL 2) by TOPRNS_1:25;
hence contradiction by A1, A6; :: thesis: verum

end;

|.r.| ^2 = ((r `1 ) ^2 ) + ((r `2 ) ^2 ) by JGRAPH_3:10;
then A9: ((r `1 ) - |.r.|) * ((r `1 ) + |.r.|) = - ((r `2 ) ^2 ) ;
(r `2 ) ^2 >= 0 by XREAL_1:65;
then - ((r `2 ) ^2 ) <= 0 ;
then ( - |.r.| <= r `1 & r `1 <= |.r.| ) by A9, XREAL_1:95;
then (r `1 ) / |.r.| <= |.r.| / |.r.| by XREAL_1:74;
then (r `1 ) / |.r.| <= 1 by A7, XCMPLX_1:60;
then A10: ((r `1 ) / |.r.|) - cn <= 1 - cn by XREAL_1:11;

A11: now

assume (1 - cn) ^2 = 0 ; :: thesis: contradiction
then (1 - cn) + cn = 0 + cn by XCMPLX_1:6;
hence contradiction by A1; :: thesis: verum

end;

A12: 1 - cn > 0 by A1, XREAL_1:151;
A13: (1 - cn) ^2 >= 0 by XREAL_1:65;
cn <= (r `1 ) / |.r.| by A1, A6;
then cn - ((r `1 ) / |.r.|) <= 0 by XREAL_1:49;
then - (cn - ((r `1 ) / |.r.|)) >= - (1 - cn) by A12, XREAL_1:26;
then (((r `1 ) / |.r.|) - cn) ^2 <= (1 - cn) ^2 by A10, SQUARE_1:119;
then ((((r `1 ) / |.r.|) - cn) ^2 ) / ((1 - cn) ^2 ) <= ((1 - cn) ^2 ) / ((1 - cn) ^2 ) by A13, XREAL_1:74;
then ((((r `1 ) / |.r.|) - cn) ^2 ) / ((1 - cn) ^2 ) <= 1 by A11, XCMPLX_1:60;
then ((((r `1 ) / |.r.|) - cn) / (1 - cn)) ^2 <= 1 by XCMPLX_1:77;
then 1 - (((((r `1 ) / |.r.|) - cn) / (1 - cn)) ^2 ) >= 0 by XREAL_1:50;
then abs (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 (abs (1 - (((((r `1 ) / |.r.|) - cn) / (1 - cn)) ^2 )))) by A1, A6;
A15: g2 . s = proj1 . s by Lm2;
A16: g1 . s = (2 NormF ) . s by Lm5;
A17: proj1 . r = r `1 by PSCOMP_1:def 28;
(2 NormF ) . r = |.r.| by Def1;
hence f . x = g3 . x by A3, A14, A15, A16, A17; :: thesis: verum

end;

hence f is continuous by A3, A5, FUNCT_1:9; :: thesis: verum