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 * (((r1 / r2) - a) / b) ) & 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 * (((r1 / r2) - a) / b) ) & 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 * (((r1 / r2) - a) / b) ) & g is continuous ) )
assume that
A1: f1 is continuous and
A2: f2 is continuous and
A3: b <> 0 and
A4: 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 * (((r1 / r2) - a) / b) ) & g is continuous )
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 & f2 . p = r0 holds
g3 . p = r1 / r0 and
A6: g3 is continuous by A1, A2, A4, JGRAPH_2:27;
consider g1 being Function of X,R^1 such that
A7: for p being Point of X holds
( g1 . p = b & g1 is continuous ) by JGRAPH_2:20;
consider g2 being Function of X,R^1 such that
A8: for p being Point of X holds
( g2 . p = a & g2 is continuous ) by JGRAPH_2:20;
consider g4 being Function of X,R^1 such that
A9: for p being Point of X
for r1, r0 being Real st g3 . p = r1 & g2 . p = r0 holds
g4 . p = r1 - r0 and
A10: g4 is continuous by A8, A6, JGRAPH_2:21;
for q being Point of X holds g1 . q <> 0 by A3, A7;
then consider g5 being Function of X,R^1 such that
A11: for p being Point of X
for r1, r0 being Real st g4 . p = r1 & g1 . p = r0 holds
g5 . p = r1 / r0 and
A12: g5 is continuous by A7, A10, JGRAPH_2:27;
consider g6 being Function of X,R^1 such that
A13: for p being Point of X
for r1, r0 being Real st f2 . p = r1 & g5 . p = r0 holds
g6 . p = r1 * r0 and
A14: g6 is continuous by A2, A12, JGRAPH_2:25;
for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g6 . p = r2 * (((r1 / r2) - a) / b)

proof

let p be Point of X; :: thesis: for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g6 . p = r2 * (((r1 / r2) - a) / b)
let r1, r2 be Real; :: thesis: ( f1 . p = r1 & f2 . p = r2 implies g6 . p = r2 * (((r1 / r2) - a) / b) )
assume that
A15: f1 . p = r1 and
A16: f2 . p = r2 ; :: thesis: g6 . p = r2 * (((r1 / r2) - a) / b)
A17: g2 . p = a by A8;
set r8 = r1 / r2;
A18: g1 . p = b by A7;
g3 . p = r1 / r2 by A5, A15, A16;
then g4 . p = (r1 / r2) - a by A9, A17;
then g5 . p = ((r1 / r2) - a) / b by A11, A18;
hence g6 . p = r2 * (((r1 / r2) - a) / b) by A13, A16; :: 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 * (((r1 / r2) - a) / b) ) & g is continuous ) by A14; :: thesis: verum