let sn 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 sn < 1 & ( 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); :: thesis: 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.| * ((((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; :: thesis: ( sn < 1 & ( 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: 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.| * ((((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) ) ; :: thesis: 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 * (((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;
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 reconsider s = x as Point of ((TOP-REAL 2) | K1) ;
x in K1 by A7, A8, A9, PRE_TOPC:8;
then reconsider r = x as Point of (TOP-REAL 2) ;
A10: ( proj2 . r = r `2 & (2 NormF) . r = |.r.| ) by Def1, PSCOMP_1:def 6;
A11: ( g2 . s = proj2 . s & g1 . s = (2 NormF) . s ) by Lm3, Lm5;
f . r = |.r.| * ((((r `2) / |.r.|) - sn) / (1 - sn)) by A2, A9;
hence f . x = g3 . x by A5, A11, A10; :: thesis: verum

end;

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