let sn be Real; for K1 being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K1),R^1 st sn < 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 `2) / |.p.|) - sn) / (1 - sn)) ^2)))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & (q `2) / |.q.| >= sn & q <> 0. (TOP-REAL 2) ) ) holds
f is continuous
let K1 be non empty Subset of (TOP-REAL 2); for f being Function of ((TOP-REAL 2) | K1),R^1 st sn < 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 `2) / |.p.|) - sn) / (1 - sn)) ^2)))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & (q `2) / |.q.| >= sn & q <> 0. (TOP-REAL 2) ) ) holds
f is continuous
let f be Function of ((TOP-REAL 2) | K1),R^1; ( sn < 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 `2) / |.p.|) - sn) / (1 - sn)) ^2)))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & (q `2) / |.q.| >= sn & 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 = sn;
set b = 1 - sn;
reconsider g2 = proj2 | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm3;
assume that
A1:
sn < 1
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 `2) / |.p.|) - sn) / (1 - sn)) ^2))))
and
A3:
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & (q `2) / |.q.| >= sn & q <> 0. (TOP-REAL 2) )
; f is continuous
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 A4:
for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0
by Lm6;
1 - sn > 0
by A1, XREAL_1:149;
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) - sn) / (1 - sn)) ^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 ;
( x in dom f implies f . x = g3 . x )
A9:
1
- sn > 0
by A1, XREAL_1:149;
assume A10:
x in dom f
;
f . x = g3 . x
then
x in K1
by A7, A8, PRE_TOPC:8;
then reconsider r =
x as
Point of
(TOP-REAL 2) ;
A11:
|.r.| <> 0
by A3, A10, TOPRNS_1:24;
|.r.| ^2 = ((r `1) ^2) + ((r `2) ^2)
by JGRAPH_3:1;
then A12:
((r `2) - |.r.|) * ((r `2) + |.r.|) = - ((r `1) ^2)
;
(r `1) ^2 >= 0
by XREAL_1:63;
then
r `2 <= |.r.|
by A12, XREAL_1:93;
then
(r `2) / |.r.| <= |.r.| / |.r.|
by XREAL_1:72;
then
(r `2) / |.r.| <= 1
by A11, XCMPLX_1:60;
then A13:
((r `2) / |.r.|) - sn <= 1
- sn
by XREAL_1:9;
reconsider s =
x as
Point of
((TOP-REAL 2) | K1) by A10;
sn - ((r `2) / |.r.|) <= 0
by A3, A10, XREAL_1:47;
then
- (sn - ((r `2) / |.r.|)) >= - (1 - sn)
by A9, XREAL_1:24;
then
(
(1 - sn) ^2 >= 0 &
(((r `2) / |.r.|) - sn) ^2 <= (1 - sn) ^2 )
by A13, SQUARE_1:49, XREAL_1:63;
then
((((r `2) / |.r.|) - sn) ^2) / ((1 - sn) ^2) <= ((1 - sn) ^2) / ((1 - sn) ^2)
by XREAL_1:72;
then
((((r `2) / |.r.|) - sn) ^2) / ((1 - sn) ^2) <= 1
by A14, XCMPLX_1:60;
then
((((r `2) / |.r.|) - sn) / (1 - sn)) ^2 <= 1
by XCMPLX_1:76;
then
1
- (((((r `2) / |.r.|) - sn) / (1 - sn)) ^2) >= 0
by XREAL_1:48;
then
|.(1 - (((((r `2) / |.r.|) - sn) / (1 - sn)) ^2)).| = 1
- (((((r `2) / |.r.|) - sn) / (1 - sn)) ^2)
by ABSVALUE:def 1;
then A15:
f . r = |.r.| * (- (sqrt |.(1 - (((((r `2) / |.r.|) - sn) / (1 - sn)) ^2)).|))
by A2, A10;
A16:
(
proj2 . r = r `2 &
(2 NormF) . r = |.r.| )
by Def1, PSCOMP_1:def 6;
(
g2 . s = proj2 . s &
g1 . s = (2 NormF) . s )
by Lm3, Lm5;
hence
f . x = g3 . x
by A5, A15, A16;
verum
end;
hence
f is continuous
by A6, A8, FUNCT_1:2; verum