let X be non empty TopSpace; :: thesis: for f1, f2 being Function of X,R^1
for a, b being Real st f1 is continuous & f2 is continuous & b <> 0 & ( 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) - a) / b) ^2)).|)) ) & g is continuous )
let f1, f2 be Function of X,R^1; :: thesis: for a, b being Real st f1 is continuous & f2 is continuous & b <> 0 & ( 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) - a) / b) ^2)).|)) ) & g is continuous )
let a, b be Real; :: thesis: ( f1 is continuous & f2 is continuous & b <> 0 & ( 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) - a) / b) ^2)).|)) ) & g is continuous ) )
assume that
A1: f1 is continuous and
A2: f2 is continuous and
A3: ( b <> 0 & ( 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 = r2 * (- (sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).|)) ) & g is continuous )
consider g1 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
g1 . p = ((r1 / r2) - a) / b and
A5: g1 is continuous by A1, A2, A3, Th4;
consider g2 being Function of X,R^1 such that
A6: for p being Point of X
for s being Real st g1 . p = s holds
g2 . p = s ^2 and
A7: g2 is continuous by A5, Th6;
consider g0 being Function of X,R^1 such that
A8: for p being Point of X holds g0 . p = 1 and
A9: g0 is continuous by JGRAPH_2:20;
consider g3 being Function of X,R^1 such that
A10: for p being Point of X
for s, t being Real st g0 . p = s & g2 . p = t holds
g3 . p = s - t and
A11: g3 is continuous by A7, A9, JGRAPH_2:21;
consider g4 being Function of X,R^1 such that
A12: for p being Point of X
for s being Real st g3 . p = s holds
g4 . p = |.s.| and
A13: g4 is continuous by A11, Th7;
for q being Point of X ex r being Real st
( g4 . q = r & r >= 0 )

proof

let q be Point of X; :: thesis: ex r being Real st
( g4 . q = r & r >= 0 )
reconsider s = g3 . q as Real ;
g4 . q = |.s.| by A12;
hence ex r being Real st
( g4 . q = r & r >= 0 ) by COMPLEX1:46; :: thesis: verum

end;

then consider g5 being Function of X,R^1 such that
A14: for p being Point of X
for s being Real st g4 . p = s holds
g5 . p = sqrt s and
A15: g5 is continuous by A13, JGRAPH_3:5;
consider g6 being Function of X,R^1 such that
A16: for p being Point of X
for s being Real st g5 . p = s holds
g6 . p = - s and
A17: g6 is continuous by A15, Th8;
consider g7 being Function of X,R^1 such that
A18: for p being Point of X
for r1, r0 being Real st f2 . p = r1 & g6 . p = r0 holds
g7 . p = r1 * r0 and
A19: g7 is continuous by A2, A17, JGRAPH_2:25;
for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g7 . p = r2 * (- (sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).|))

proof

let p be Point of X; :: thesis: for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g7 . p = r2 * (- (sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).|))
let r1, r2 be Real; :: thesis: ( f1 . p = r1 & f2 . p = r2 implies g7 . p = r2 * (- (sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).|)) )
assume that
A20: f1 . p = r1 and
A21: f2 . p = r2 ; :: thesis: g7 . p = r2 * (- (sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).|))
A22: g0 . p = 1 by A8;
g1 . p = ((r1 / r2) - a) / b by A4, A20, A21;
then g2 . p = (((r1 / r2) - a) / b) ^2 by A6;
then g3 . p = 1 - ((((r1 / r2) - a) / b) ^2) by A10, A22;
then g4 . p = |.(1 - ((((r1 / r2) - a) / b) ^2)).| by A12;
then g5 . p = sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).| by A14;
then g6 . p = - (sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).|) by A16;
hence g7 . p = r2 * (- (sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).|)) by A18, A21; :: 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 = r2 * (- (sqrt |.(1 - ((((r1 / r2) - a) / b) ^2)).|)) ) & g is continuous ) by A19; :: thesis: verum