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 Lm10, Lm11;
A2: AffineMap ((2 * PI),0) = R^1 (AffineMap ((2 * PI),0)) ;
reconsider g = CircleMap as Function of R^1,(TOP-REAL 2) 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 (dom cos)) = R^1 by Th6, SIN_COS:24;
A5: R^1 | (R^1 (dom sin)) = R^1 by Th6, SIN_COS:24;
for p being Point of R^1
for V being Subset of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 (Euclid 2) by TOPREAL3:8;
V = Int V by A7, TOPS_1:23;
then consider r being Real such that
A8: r > 0 and
A9: Ball (e,r) c= V by A6, GOBOARD6:5;
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 A4, PRE_TOPC:26;
A13: sR is continuous by A5, PRE_TOPC:26;
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 A8, SQUARE_1:19, TOPREAL6:15;
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 A2, A1, A3, A10, A13, Th5, JGRAPH_2:10;
A18: A is open by JORDAN6:35;
(g . p) `1 = (cR * l) . p by A14, EUCLID:52;
then (cR * l) . p in A by A8, SQUARE_1:19, TOPREAL6:15;
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 A2, A1, A3, A18, A12, Th5, JGRAPH_2:10;
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 A15, A19, XBOOLE_0:def 4; :: thesis: ( Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus Ws /\ Wc is open by A16, A20; :: 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 A22, XBOOLE_0:def 4;
then A24: (sR * l) . x in (sR * l) .: Ws by FUNCT_2:35;
x in Wc by A22, XBOOLE_0:def 4;
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 A17, A21, A24, A25, HILBERT3:11;
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