let X be non empty TopSpace; :: thesis: for f1 being Function of X,R^1 st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = - r1 ) & g is continuous )
let f1 be Function of X,R^1 ; :: thesis: ( f1 is continuous implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = - r1 ) & g is continuous ) )
assume A1: f1 is continuous ; :: thesis: ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = - r1 ) & g is continuous )
consider g1 being Function of X,R^1 such that
A2: ( ( for p being Point of X holds g1 . p = 0 ) & g1 is continuous ) by JGRAPH_2:30;
consider g2 being Function of X,R^1 such that
A3: ( ( for p being Point of X
for r1, r2 being real number st g1 . p = r1 & f1 . p = r2 holds
g2 . p = r1 - r2 ) & g2 is continuous ) by A1, A2, JGRAPH_2:31;
for p being Point of X
for r1 being real number st f1 . p = r1 holds
g2 . p = - r1

proof

let p be Point of X; :: thesis: for r1 being real number st f1 . p = r1 holds
g2 . p = - r1
let r1 be real number ; :: thesis: ( f1 . p = r1 implies g2 . p = - r1 )
assume A4: f1 . p = r1 ; :: thesis: g2 . p = - r1
g1 . p = 0 by A2;
then g2 . p = 0 - r1 by A3, A4;
hence g2 . p = - r1 ; :: thesis: verum

end;

hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = - r1 ) & g is continuous ) by A3; :: thesis: verum