let X be non empty TopSpace; 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 = r2 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )
let f1, f2 be Function of X,R^1; ( 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 = r2 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous ) )
assume that
A1:
f1 is continuous
and
A2:
f2 is continuous
and
A3:
for q being Point of X holds f2 . q <> 0
; 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 = r2 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )
consider g2 being Function of X,R^1 such that
A4:
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
A5:
g2 is continuous
by A1, A2, A3, Th8;
for q being Point of X holds g2 . q <> 0
then consider g3 being Function of X,R^1 such that
A6:
for p being Point of X
for r2, r0 being Real st f2 . p = r2 & g2 . p = r0 holds
g3 . p = r2 / r0
and
A7:
g3 is continuous
by A2, A5, JGRAPH_2:27;
for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g3 . p = r2 / (sqrt (1 + ((r1 / r2) ^2)))
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 = r2 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )
by A7; verum