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 st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * (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 st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous ) )

assume that
A1: f1 is continuous and
A2: ( 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 st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

consider g2 being Function of X,R^1 such that
A3: for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g2 . p = sqrt (1 + ((r1 / r2) ^2)) and
A4: g2 is continuous by A1, A2, Th8;
consider g3 being Function of X,R^1 such that
A5: for p being Point of X
for r1, r0 being Real st f1 . p = r1 & g2 . p = r0 holds
g3 . p = r1 * r0 and
A6: g3 is continuous by ;
for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g3 . p = r1 * (sqrt (1 + ((r1 / r2) ^2)))
proof
let p be Point of X; :: thesis: for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g3 . p = r1 * (sqrt (1 + ((r1 / r2) ^2)))

let r1, r2 be Real; :: thesis: ( f1 . p = r1 & f2 . p = r2 implies g3 . p = r1 * (sqrt (1 + ((r1 / r2) ^2))) )
assume that
A7: f1 . p = r1 and
A8: f2 . p = r2 ; :: thesis: g3 . p = r1 * (sqrt (1 + ((r1 / r2) ^2)))
g2 . p = sqrt (1 + ((r1 / r2) ^2)) by A3, A7, A8;
hence g3 . p = r1 * (sqrt (1 + ((r1 / r2) ^2))) by A5, A7; :: thesis: verum
end;
hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous ) by A6; :: thesis: verum