let n, m be Nat; :: thesis: for f being Function of (),() st f is continuous holds
f (-) is continuous Function of (),()

let f be Function of (),(); :: thesis: ( f is continuous implies f (-) is continuous Function of (),() )
assume A1: f is continuous ; :: thesis: f (-) is continuous Function of (),()
reconsider g = f (-) as Function of (),() by Th34;
for p being Point of ()
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 (); :: 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 ;
take s ; :: thesis: g .: (Ball (p,s)) c= Ball ((g . p),r)
let y be Element of (); :: 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 () such that
A3: x in Ball (p,s) and
A4: g . x = y by FUNCT_2:65;
dom g = the carrier of () 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 ;
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 (),() by TOPS_4:20; :: thesis: verum