let n, m be Nat; :: thesis: 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); :: thesis: ( f is continuous implies f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n) )
assume A1: f is continuous ; :: thesis: 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); :: thesis: 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; :: thesis: 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 ; :: thesis: g .: (Ball (p,s)) c= Ball ((g . p),r)
let y be Element of (TOP-REAL n); :: according to LATTICE7:def 1 :: thesis: ( not y in g .: (Ball (p,s)) or y in Ball ((g . p),r) )
assume y in g .: (Ball (p,s)) ; :: thesis: 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; :: thesis: verum

end;

hence f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n) by TOPS_4:20; :: thesis: verum