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) )

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

hence
f (-) is continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),(TOP-REAL m)
by TOPS_4:18; :: thesis: verum
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;( 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