let K1 be non empty Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

let f be Function of ((TOP-REAL 2) | K1),R^1; :: thesis: ( ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) implies f is continuous )

reconsider g1 = proj1 | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm7;

reconsider g2 = proj2 | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm5;

assume that

A1: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) and

A2: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ; :: thesis: f is continuous

A3: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

A4: 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) ^2))) and

A5: g3 is continuous by Th10;

A6: for x being object st x in dom f holds

f . x = g3 . x

then dom f = dom g3 by FUNCT_2:def 1;

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

f . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

let f be Function of ((TOP-REAL 2) | K1),R^1; :: thesis: ( ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) implies f is continuous )

reconsider g1 = proj1 | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm7;

reconsider g2 = proj2 | K1 as continuous Function of ((TOP-REAL 2) | K1),R^1 by Lm5;

assume that

A1: for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) and

A2: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ; :: thesis: f is continuous

A3: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;

now :: thesis: for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0

then consider g3 being Function of ((TOP-REAL 2) | K1),R^1 such that let q be Point of ((TOP-REAL 2) | K1); :: thesis: g1 . q <> 0

q in the carrier of ((TOP-REAL 2) | K1) ;

then reconsider q2 = q as Point of (TOP-REAL 2) by A3;

g1 . q = proj1 . q by Lm6

.= q2 `1 by PSCOMP_1:def 5 ;

hence g1 . q <> 0 by A2; :: thesis: verum

end;q in the carrier of ((TOP-REAL 2) | K1) ;

then reconsider q2 = q as Point of (TOP-REAL 2) by A3;

g1 . q = proj1 . q by Lm6

.= q2 `1 by PSCOMP_1:def 5 ;

hence g1 . q <> 0 by A2; :: thesis: verum

A4: 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) ^2))) and

A5: g3 is continuous by Th10;

A6: for x being object st x in dom f holds

f . x = g3 . x

proof

dom g3 = the carrier of ((TOP-REAL 2) | K1)
by FUNCT_2:def 1;
let x be object ; :: thesis: ( x in dom f implies f . x = g3 . x )

assume A7: x in dom f ; :: thesis: f . x = g3 . x

then reconsider s = x as Point of ((TOP-REAL 2) | K1) ;

x in the carrier of ((TOP-REAL 2) | K1) by A7;

then x in K1 by PRE_TOPC:8;

then reconsider r = x as Point of (TOP-REAL 2) ;

A8: ( proj2 . r = r `2 & proj1 . r = r `1 ) by PSCOMP_1:def 5, PSCOMP_1:def 6;

A9: ( g2 . s = proj2 . s & g1 . s = proj1 . s ) by Lm4, Lm6;

f . r = (r `1) / (sqrt (1 + (((r `2) / (r `1)) ^2))) by A1, A7;

hence f . x = g3 . x by A4, A9, A8; :: thesis: verum

end;assume A7: x in dom f ; :: thesis: f . x = g3 . x

then reconsider s = x as Point of ((TOP-REAL 2) | K1) ;

x in the carrier of ((TOP-REAL 2) | K1) by A7;

then x in K1 by PRE_TOPC:8;

then reconsider r = x as Point of (TOP-REAL 2) ;

A8: ( proj2 . r = r `2 & proj1 . r = r `1 ) by PSCOMP_1:def 5, PSCOMP_1:def 6;

A9: ( g2 . s = proj2 . s & g1 . s = proj1 . s ) by Lm4, Lm6;

f . r = (r `1) / (sqrt (1 + (((r `2) / (r `1)) ^2))) by A1, A7;

hence f . x = g3 . x by A4, A9, A8; :: thesis: verum

then dom f = dom g3 by FUNCT_2:def 1;

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