let X be non empty TopSpace; :: thesis: for f1, f2 being Function of X,R^1
for a, b being real number 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 number st f1 . p = r1 & f2 . p = r2 holds
g . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 ))))) ) & g is continuous )
let f1, f2 be Function of X,R^1 ; :: thesis: for a, b being real number 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 number st f1 . p = r1 & f2 . p = r2 holds
g . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 ))))) ) & g is continuous )
let a, b be real number ; :: 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 number st f1 . p = r1 & f2 . p = r2 holds
g . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 ))))) ) & g is continuous ) )
assume A1: ( f1 is continuous & f2 is continuous & 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 number st f1 . p = r1 & f2 . p = r2 holds
g . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 ))))) ) & g is continuous )
then consider g1 being Function of X,R^1 such that
A2: ( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g1 . p = ((r1 / r2) - a) / b ) & g1 is continuous ) by Th9;
consider g2 being Function of X,R^1 such that
A3: ( ( for p being Point of X
for s being real number st g1 . p = s holds
g2 . p = s ^2 ) & g2 is continuous ) by A2, Th11;
consider g0 being Function of X,R^1 such that
A4: ( ( for p being Point of X holds g0 . p = 1 ) & g0 is continuous ) by JGRAPH_2:30;
consider g3 being Function of X,R^1 such that
A5: ( ( for p being Point of X
for s, t being real number st g0 . p = s & g2 . p = t holds
g3 . p = s - t ) & g3 is continuous ) by A3, A4, JGRAPH_2:31;
consider g4 being Function of X,R^1 such that
A6: ( ( for p being Point of X
for s being real number st g3 . p = s holds
g4 . p = abs s ) & g4 is continuous ) by A5, Th12;
for q being Point of X ex r being real number st
( g4 . q = r & r >= 0 )

proof

let q be Point of X; :: thesis: ex r being real number st
( g4 . q = r & r >= 0 )
reconsider s = g3 . q as Real by TOPMETR:24;
g4 . q = abs s by A6;
hence ex r being real number st
( g4 . q = r & r >= 0 ) by COMPLEX1:132; :: thesis: verum

end;

then consider g5 being Function of X,R^1 such that
A7: ( ( for p being Point of X
for s being real number st g4 . p = s holds
g5 . p = sqrt s ) & g5 is continuous ) by A6, JGRAPH_3:15;
consider g6 being Function of X,R^1 such that
A8: ( ( for p being Point of X
for s being real number st g5 . p = s holds
g6 . p = - s ) & g6 is continuous ) by A7, Th13;
consider g7 being Function of X,R^1 such that
A9: ( ( for p being Point of X
for r1, r0 being real number st f2 . p = r1 & g6 . p = r0 holds
g7 . p = r1 * r0 ) & g7 is continuous ) by A1, A8, JGRAPH_2:35;
for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g7 . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 )))))

proof

let p be Point of X; :: thesis: for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g7 . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 )))))
let r1, r2 be real number ; :: thesis: ( f1 . p = r1 & f2 . p = r2 implies g7 . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 ))))) )
assume A10: ( f1 . p = r1 & f2 . p = r2 ) ; :: thesis: g7 . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 )))))
A11: g0 . p = 1 by A4;
g1 . p = ((r1 / r2) - a) / b by A2, A10;
then g2 . p = (((r1 / r2) - a) / b) ^2 by A3;
then g3 . p = 1 - ((((r1 / r2) - a) / b) ^2 ) by A5, A11;
then g4 . p = abs (1 - ((((r1 / r2) - a) / b) ^2 )) by A6;
then g5 . p = sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 ))) by A7;
then g6 . p = - (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 )))) by A8;
hence g7 . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 ))))) by A9, A10; :: 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 = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2 ))))) ) & g is continuous ) by A9; :: thesis: verum