let X be non empty TopSpace; :: thesis: for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous )

let f1 be Function of X,R^1; :: thesis: for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous )

let a be Real; :: thesis: ( f1 is continuous implies ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous ) )

assume f1 is continuous ; :: thesis: ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous )

then consider g1 being Function of X,R^1 such that

A1: for p being Point of X

for r1 being Real st f1 . p = r1 holds

g1 . p = r1 + (- a) and

A2: g1 is continuous by JGRAPH_2:24;

for p being Point of X

for r1 being Real st f1 . p = r1 holds

g1 . p = r1 - a

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous ) by A2; :: thesis: verum

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous )

let f1 be Function of X,R^1; :: thesis: for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous )

let a be Real; :: thesis: ( f1 is continuous implies ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous ) )

assume f1 is continuous ; :: thesis: ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous )

then consider g1 being Function of X,R^1 such that

A1: for p being Point of X

for r1 being Real st f1 . p = r1 holds

g1 . p = r1 + (- a) and

A2: g1 is continuous by JGRAPH_2:24;

for p being Point of X

for r1 being Real st f1 . p = r1 holds

g1 . p = r1 - a

proof

hence
ex g being Function of X,R^1 st
let p be Point of X; :: thesis: for r1 being Real st f1 . p = r1 holds

g1 . p = r1 - a

let r1 be Real; :: thesis: ( f1 . p = r1 implies g1 . p = r1 - a )

assume f1 . p = r1 ; :: thesis: g1 . p = r1 - a

then g1 . p = r1 + (- a) by A1;

hence g1 . p = r1 - a ; :: thesis: verum

end;g1 . p = r1 - a

let r1 be Real; :: thesis: ( f1 . p = r1 implies g1 . p = r1 - a )

assume f1 . p = r1 ; :: thesis: g1 . p = r1 - a

then g1 . p = r1 + (- a) by A1;

hence g1 . p = r1 - a ; :: thesis: verum

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous ) by A2; :: thesis: verum