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 = a - r1 ) & 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 = a - r1 ) & 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 = a - r1 ) & 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 = a - r1 ) & 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 Th7;

consider g2 being Function of X,R^1 such that

A3: for p being Point of X

for r1 being Real st g1 . p = r1 holds

g2 . p = - r1 and

A4: g2 is continuous by A2, JGRAPH_4:8;

for p being Point of X

for r1 being Real st f1 . p = r1 holds

g2 . p = a - r1

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = a - r1 ) & g is continuous ) by A4; :: 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 = a - r1 ) & 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 = a - r1 ) & 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 = a - r1 ) & 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 = a - r1 ) & 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 Th7;

consider g2 being Function of X,R^1 such that

A3: for p being Point of X

for r1 being Real st g1 . p = r1 holds

g2 . p = - r1 and

A4: g2 is continuous by A2, JGRAPH_4:8;

for p being Point of X

for r1 being Real st f1 . p = r1 holds

g2 . p = a - r1

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

g2 . p = a - r1

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

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

then g1 . p = r1 - a by A1;

then g2 . p = - (r1 - a) by A3

.= a - r1 ;

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

end;g2 . p = a - r1

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

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

then g1 . p = r1 - a by A1;

then g2 . p = - (r1 - a) by A3

.= a - r1 ;

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

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

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