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 - 1 < sn & ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & 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 - 1 < sn & ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & q <> 0. (TOP-REAL 2) ) ) holds
f is continuous
let f be Function of ((TOP-REAL 2) | K1),R^1; ( - 1 < sn & ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & 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:
- 1 < sn
and
A2:
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn))
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 <> 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:148;
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 * (((r1 / r2) - sn) / (1 + sn))
and
A6:
g3 is continuous
by A4, Th5;
A7:
dom g3 = the carrier of ((TOP-REAL 2) | K1)
by FUNCT_2:def 1;
A8:
for x being object st x in dom f holds
f . x = g3 . x
dom f = dom g3
by A7, FUNCT_2:def 1;
hence
f is continuous
by A6, A8, FUNCT_1:2; verum