let n, m be Nat; for f being Function of (TOP-REAL m),(TOP-REAL n) st f is continuous holds
f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n)
let f be Function of (TOP-REAL m),(TOP-REAL n); ( f is continuous implies f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n) )
assume A1:
f is continuous
; f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n)
reconsider g = f (-) as Function of (TOP-REAL m),(TOP-REAL n) by Th34;
for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st g .: (Ball (p,s)) c= Ball ((g . p),r)
proof
let p be
Point of
(TOP-REAL m);
for r being positive Real ex s being positive Real st g .: (Ball (p,s)) c= Ball ((g . p),r)let r be
positive Real;
ex s being positive Real st g .: (Ball (p,s)) c= Ball ((g . p),r)
consider s being
positive Real such that A2:
f .: (Ball ((- p),s)) c= Ball (
(f . (- p)),
r)
by A1, TOPS_4:20;
take
s
;
g .: (Ball (p,s)) c= Ball ((g . p),r)
let y be
Element of
(TOP-REAL n);
LATTICE7:def 1 ( not y in g .: (Ball (p,s)) or y in Ball ((g . p),r) )
assume
y in g .: (Ball (p,s))
;
y in Ball ((g . p),r)
then consider x being
Element of
(TOP-REAL m) such that A3:
x in Ball (
p,
s)
and A4:
g . x = y
by FUNCT_2:65;
dom g = the
carrier of
(TOP-REAL m)
by FUNCT_2:def 1;
then A5:
(
g . x = f . (- x) &
g . p = f . (- p) )
by VALUED_2:def 34;
- x in Ball (
(- p),
s)
by A3, Th23;
then
f . (- x) in f .: (Ball ((- p),s))
by FUNCT_2:35;
hence
y in Ball (
(g . p),
r)
by A2, A4, A5;
verum
end;
hence
f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n)
by TOPS_4:20; verum