let m, n 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 real positive number ex s being real positive number st g .: (Ball p,s) c= Ball (g . p),r

proof

let p be Point of (TOP-REAL m); :: thesis: for r being real positive number ex s being real positive number st g .: (Ball p,s) c= Ball (g . p),r
let r be real positive number ; :: thesis: ex s being real positive number st g .: (Ball p,s) c= Ball (g . p),r
consider s being real positive number 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:116;
dom g = the carrier of (TOP-REAL m) by FUNCT_2:def 1;
then A6: ( 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:43;
hence y in Ball (g . p),r by A2, A4, A6; :: thesis: verum

end;

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