let m be Nat; :: thesis: for r being non negative Real
for f being continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),() holds f (-) is continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),()

let r be non negative Real; :: thesis: for f being continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),() holds f (-) is continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),()
set T = Tcircle ((0. (TOP-REAL (m + 1))),r);
let f be continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),(); :: thesis: f (-) is continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),()
reconsider g = f (-) as Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),() by Th61;
for p being Point of (Tcircle ((0. (TOP-REAL (m + 1))),r))
for r being positive Real 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 positive Real 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 positive Real; :: 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 ;
hence p in W1 ; :: thesis: g .: W1 c= Ball ((g . p),r)
let y be Element of (); :: 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:65;
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 ;
then f . (- x) in f .: W by FUNCT_2:35;
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)),() by TOPS_4:18; :: thesis: verum