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 = 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 = 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 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 st f1 . p = r1 & f2 . p = r2 holds

g2 . p = 1 + ((r1 / r2) ^2) and

A2: g2 is continuous by Th7;

for q being Point of X ex r being Real st

( g2 . q = r & r >= 0 )

A3: for p being Point of X

for r1 being Real st g2 . p = r1 holds

g3 . p = sqrt r1 and

A4: g3 is continuous by A2, Th5;

for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g3 . p = sqrt (1 + ((r1 / r2) ^2))

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = sqrt (1 + ((r1 / r2) ^2)) ) & g is continuous ) by A4; :: thesis: verum

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 = 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 = 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 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 st f1 . p = r1 & f2 . p = r2 holds

g2 . p = 1 + ((r1 / r2) ^2) and

A2: g2 is continuous by Th7;

for q being Point of X ex r being Real st

( g2 . q = r & r >= 0 )

proof

then consider g3 being Function of X,R^1 such that
let q be Point of X; :: thesis: ex r being Real st

( g2 . q = r & r >= 0 )

reconsider r1 = f1 . q, r2 = f2 . q as Real ;

1 + ((r1 / r2) ^2) > 0 by Lm1;

hence ex r being Real st

( g2 . q = r & r >= 0 ) by A1; :: thesis: verum

end;( g2 . q = r & r >= 0 )

reconsider r1 = f1 . q, r2 = f2 . q as Real ;

1 + ((r1 / r2) ^2) > 0 by Lm1;

hence ex r being Real st

( g2 . q = r & r >= 0 ) by A1; :: thesis: verum

A3: for p being Point of X

for r1 being Real st g2 . p = r1 holds

g3 . p = sqrt r1 and

A4: g3 is continuous by A2, Th5;

for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g3 . p = sqrt (1 + ((r1 / r2) ^2))

proof

hence
ex g being Function of X,R^1 st
let p be Point of X; :: thesis: for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g3 . p = sqrt (1 + ((r1 / r2) ^2))

let r1, r2 be Real; :: 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 A3; :: thesis: verum

end;g3 . p = sqrt (1 + ((r1 / r2) ^2))

let r1, r2 be Real; :: 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 A3; :: thesis: verum

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = sqrt (1 + ((r1 / r2) ^2)) ) & g is continuous ) by A4; :: thesis: verum