let X be non empty TopSpace; :: thesis: for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = sqrt (1 + ((r1 / r2) ^2 )) ) & g is continuous )
let f1, f2 be Function of X,R^1 ; :: thesis: ( f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = sqrt (1 + ((r1 / r2) ^2 )) ) & g is continuous ) )
assume ( f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) ) ; :: thesis: ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = sqrt (1 + ((r1 / r2) ^2 )) ) & g is continuous )
then consider g2 being Function of X,R^1 such that
A1: ( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g2 . p = 1 + ((r1 / r2) ^2 ) ) & g2 is continuous ) by Th17;
for q being Point of X ex r being real number st
( g2 . q = r & r >= 0 )

proof

let q be Point of X; :: thesis: ex r being real number st
( g2 . q = r & r >= 0 )
reconsider r1 = f1 . q, r2 = f2 . q as Real by TOPMETR:24;
1 + ((r1 / r2) ^2 ) > 0 by Lm1;
hence ex r being real number st
( g2 . q = r & r >= 0 ) by A1; :: thesis: verum

end;

then consider g3 being Function of X,R^1 such that
A2: ( ( for p being Point of X
for r1 being real number st g2 . p = r1 holds
g3 . p = sqrt r1 ) & g3 is continuous ) by A1, Th15;
for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g3 . p = sqrt (1 + ((r1 / r2) ^2 ))

proof

let p be Point of X; :: thesis: for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g3 . p = sqrt (1 + ((r1 / r2) ^2 ))
let r1, r2 be real number ; :: thesis: ( f1 . p = r1 & f2 . p = r2 implies g3 . p = sqrt (1 + ((r1 / r2) ^2 )) )
assume ( f1 . p = r1 & f2 . p = r2 ) ; :: thesis: g3 . p = sqrt (1 + ((r1 / r2) ^2 ))
then g2 . p = 1 + ((r1 / r2) ^2 ) by A1;
hence g3 . p = sqrt (1 + ((r1 / r2) ^2 )) by A2; :: thesis: verum

end;

hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = sqrt (1 + ((r1 / r2) ^2 )) ) & g is continuous ) by A2; :: thesis: verum