let X be non empty TopSpace; 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 st f1 . p = r1 holds
g . p = - r1 ) & g is continuous )
let f1 be Function of X,R^1; ( 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 ) & g is continuous ) )
consider g1 being Function of X,R^1 such that
A1:
for p being Point of X holds g1 . p = 0
and
A2:
g1 is continuous
by JGRAPH_2:20;
assume
f1 is continuous
; 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 ) & g is continuous )
then consider g2 being Function of X,R^1 such that
A3:
for p being Point of X
for r1, r2 being Real st g1 . p = r1 & f1 . p = r2 holds
g2 . p = r1 - r2
and
A4:
g2 is continuous
by A2, JGRAPH_2:21;
for p being Point of X
for r1 being Real st f1 . p = r1 holds
g2 . p = - r1
proof
let p be
Point of
X;
for r1 being Real st f1 . p = r1 holds
g2 . p = - r1let r1 be
Real;
( f1 . p = r1 implies g2 . p = - r1 )
assume A5:
f1 . p = r1
;
g2 . p = - r1
g1 . p = 0
by A1;
then
g2 . p = 0 - r1
by A3, A5;
hence
g2 . p = - r1
;
verum
end;
hence
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 ) & g is continuous )
by A4; verum