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)

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

hence
f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n)
by TOPS_4:20; :: thesis: verum
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;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