let X be non empty TopSpace; 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 = ((r1 / r2) - a) / b ) & g is continuous )
let f1, f2 be 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 = ((r1 / r2) - a) / b ) & g is continuous )
let a, b be Real; ( 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 = ((r1 / r2) - a) / b ) & g is continuous ) )
assume that
A1:
( f1 is continuous & f2 is continuous )
and
A2:
b <> 0
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 = ((r1 / r2) - a) / b ) & g is continuous )
consider g3 being Function of X,R^1 such that
A4:
for p being Point of X
for r1, r0 being Real st f1 . p = r1 & f2 . p = r0 holds
g3 . p = r1 / r0
and
A5:
g3 is continuous
by A1, A3, JGRAPH_2:27;
consider g1 being Function of X,R^1 such that
A6:
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
A7:
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
A8:
for p being Point of X
for r1, r0 being Real st g3 . p = r1 & g2 . p = r0 holds
g4 . p = r1 - r0
and
A9:
g4 is continuous
by A7, A5, JGRAPH_2:21;
for q being Point of X holds g1 . q <> 0
by A2, A6;
then consider g5 being Function of X,R^1 such that
A10:
for p being Point of X
for r1, r0 being Real st g4 . p = r1 & g1 . p = r0 holds
g5 . p = r1 / r0
and
A11:
g5 is continuous
by A6, A9, JGRAPH_2:27;
for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g5 . p = ((r1 / r2) - a) / b
proof
let p be
Point of
X;
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g5 . p = ((r1 / r2) - a) / blet r1,
r2 be
Real;
( f1 . p = r1 & f2 . p = r2 implies g5 . p = ((r1 / r2) - a) / b )
set r8 =
r1 / r2;
A12:
g1 . p = b
by A6;
assume
(
f1 . p = r1 &
f2 . p = r2 )
;
g5 . p = ((r1 / r2) - a) / b
then A13:
g3 . p = r1 / r2
by A4;
g2 . p = a
by A7;
then
g4 . p = (r1 / r2) - a
by A8, A13;
hence
g5 . p = ((r1 / r2) - a) / b
by A10, A12;
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 = ((r1 / r2) - a) / b ) & g is continuous )
by A11; verum