reconsider l = AffineMap ((2 * PI),0) as Function of R^1,R^1 by Th8;
set sR = R^1 sin;
set cR = R^1 cos;
A1: dom (AffineMap ((2 * PI),0)) = REAL by FUNCT_2:def 1;
reconsider sR = R^1 sin, cR = R^1 cos as Function of R^1,R^1 by ;
A2: AffineMap ((2 * PI),0) = R^1 (AffineMap ((2 * PI),0)) ;
reconsider g = CircleMap as Function of R^1,() by TOPREALA:7;
A3: rng (AffineMap ((2 * PI),0)) = [#] REAL by FCONT_1:55;
set c = cR * l;
set s = sR * l;
A4: R^1 | (R^1 ()) = R^1 by ;
A5: R^1 | (R^1 ()) = R^1 by ;
for p being Point of R^1
for V being Subset of () st g . p in V & V is open holds
ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )
proof
let p be Point of R^1; :: thesis: for V being Subset of () st g . p in V & V is open holds
ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )

let V be Subset of (); :: thesis: ( g . p in V & V is open implies ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V ) )

assume that
A6: g . p in V and
A7: V is open ; :: thesis: ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )

reconsider e = g . p as Point of () by TOPREAL3:8;
V = Int V by ;
then consider r being Real such that
A8: r > 0 and
A9: Ball (e,r) c= V by ;
set B = ].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[;
set A = ].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[;
set F = (1,2) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[);
reconsider A = ].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[, B = ].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[ as Subset of R^1 by TOPMETR:17;
A10: B is open by JORDAN6:35;
A11: product ((1,2) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[)) c= Ball (e,r) by TOPREAL6:41;
A12: cR is continuous by ;
A13: sR is continuous by ;
A14: g . p = |[((cR * l) . p),((sR * l) . p)]| by Lm20;
then (g . p) `2 = (sR * l) . p by EUCLID:52;
then (sR * l) . p in B by ;
then consider Ws being Subset of R^1 such that
A15: p in Ws and
A16: Ws is open and
A17: (sR * l) .: Ws c= B by ;
A18: A is open by JORDAN6:35;
(g . p) `1 = (cR * l) . p by ;
then (cR * l) . p in A by ;
then consider Wc being Subset of R^1 such that
A19: p in Wc and
A20: Wc is open and
A21: (cR * l) .: Wc c= A by ;
set W = Ws /\ Wc;
take Ws /\ Wc ; :: thesis: ( p in Ws /\ Wc & Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus p in Ws /\ Wc by ; :: thesis: ( Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus Ws /\ Wc is open by ; :: thesis: g .: (Ws /\ Wc) c= V
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g .: (Ws /\ Wc) or y in V )
assume y in g .: (Ws /\ Wc) ; :: thesis: y in V
then consider x being Element of R^1 such that
A22: x in Ws /\ Wc and
A23: y = g . x by FUNCT_2:65;
x in Ws by ;
then A24: (sR * l) . x in (sR * l) .: Ws by FUNCT_2:35;
x in Wc by ;
then A25: (cR * l) . x in (cR * l) .: Wc by FUNCT_2:35;
|[((cR * l) . x),((sR * l) . x)]| = (1,2) --> (((cR * l) . x),((sR * l) . x)) by TOPREALA:28;
then |[((cR * l) . x),((sR * l) . x)]| in product ((1,2) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[)) by ;
then A26: |[((cR * l) . x),((sR * l) . x)]| in Ball (e,r) by A11;
g . x = |[((cR * l) . x),((sR * l) . x)]| by Lm20;
hence y in V by A9, A23, A26; :: thesis: verum
end;
then g is continuous by JGRAPH_2:10;
hence CircleMap is continuous by PRE_TOPC:27; :: thesis: verum