let m be Nat; :: thesis: for r being real non negative number
for f being continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m) holds f (-) is continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m)
let r be real non negative number ; :: thesis: for f being continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m) holds f (-) is continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m)
set T = Tcircle (0. (TOP-REAL (m + 1))),r;
let f be continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m); :: thesis: f (-) is continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m)
reconsider g = f (-) as Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m) by Th61;
for p being Point of (Tcircle (0. (TOP-REAL (m + 1))),r)
for r being real positive number ex W being open Subset of (Tcircle (0. (TOP-REAL (m + 1))),r) st
( p in W & g .: W c= Ball (g . p),r )

proof

let p be Point of (Tcircle (0. (TOP-REAL (m + 1))),r); :: thesis: for r being real positive number ex W being open Subset of (Tcircle (0. (TOP-REAL (m + 1))),r) st
( p in W & g .: W c= Ball (g . p),r )
let r be real positive number ; :: thesis: ex W being open Subset of (Tcircle (0. (TOP-REAL (m + 1))),r) st
( p in W & g .: W c= Ball (g . p),r )
reconsider q = - p as Point of (Tcircle (0. (TOP-REAL (m + 1))),r) by Th60;
consider W being open Subset of (Tcircle (0. (TOP-REAL (m + 1))),r) such that
A1: q in W and
A2: f .: W c= Ball (f . q),r by TOPS_4:18;
reconsider W1 = (-) W as open Subset of (Tcircle (0. (TOP-REAL (m + 1))),r) ;
take W1 ; :: thesis: ( p in W1 & g .: W1 c= Ball (g . p),r )
- q in W1 by A1, Def3;
hence p in W1 ; :: thesis: g .: W1 c= Ball (g . p),r
let y be Element of (TOP-REAL m); :: according to LATTICE7:def 1 :: thesis: ( not y in g .: W1 or y in Ball (g . p),r )
assume y in g .: W1 ; :: thesis: y in Ball (g . p),r
then consider x being Element of (Tcircle (0. (TOP-REAL (m + 1))),r) such that
A3: x in W1 and
A4: g . x = y by FUNCT_2:116;
dom g = the carrier of (Tcircle (0. (TOP-REAL (m + 1))),r) by FUNCT_2:def 1;
then A5: ( g . x = f . (- x) & g . p = f . (- p) ) by VALUED_2:def 34;
- x in (-) W1 by A3, Def3;
then f . (- x) in f .: W by FUNCT_2:43;
hence y in Ball (g . p),r by A2, A4, A5; :: thesis: verum

end;

hence f (-) is continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m) by TOPS_4:18; :: thesis: verum