let m be Nat; :: thesis: for r being non negative Real
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 non negative Real; :: 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 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 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: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 A3, Def3;
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)),(TOP-REAL m) by TOPS_4:18; :: thesis: verum