A1: AffineMap (2 * PI ),0 = R^1 (AffineMap (2 * PI ),0 ) ;
A2: R^1 | (R^1 (dom sin )) = R^1 by Th6, SIN_COS:27;
A3: R^1 | (R^1 (dom cos )) = R^1 by Th6, SIN_COS:27;
set sR = R^1 sin ;
set cR = R^1 cos ;
reconsider sR = R^1 sin , cR = R^1 cos as Function of R^1 ,R^1 by Lm11, Lm12;
reconsider l = AffineMap (2 * PI ),0 as Function of R^1 ,R^1 by Th8;
A4: dom (AffineMap (2 * PI ),0 ) = REAL by FUNCT_2:def 1;
A5: rng (AffineMap (2 * PI ),0 ) = [#] REAL by JORDAN16:32;
set s = sR * l;
set c = cR * l;
reconsider g = CircleMap as Function of R^1 ,(TOP-REAL 2) by TOPREALA:28;
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 )
A8: V = Int V by A7, TOPS_1:55;
reconsider e = g . p as Point of (Euclid 2) by TOPREAL3:13;
consider r being real number such that
A9: r > 0 and
A10: Ball e,r c= V by A6, A8, GOBOARD6:8;
set A = ].(((g . p) `1 ) - (r / (sqrt 2))),(((g . p) `1 ) + (r / (sqrt 2))).[;
set B = ].(((g . p) `2 ) - (r / (sqrt 2))),(((g . p) `2 ) + (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))).[;
A12: 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:49;
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:24;
A13: B is open by JORDAN6:46;
A14: g . p = |[((cR * l) . p),((sR * l) . p)]| by Lm22;
then A15: (g . p) `2 = (sR * l) . p by EUCLID:56;
B16: sR is continuous by A2, PRE_TOPC:56;
(sR * l) . p in B by A9, A15, SQUARE_1:84, TOPREAL6:20;
then consider Ws being Subset of R^1 such that
A17: p in Ws and
A18: Ws is open and
A19: (sR * l) .: Ws c= B by A13, B16, A1, A4, A5, Th5, JGRAPH_2:20;
A20: A is open by JORDAN6:46;
A21: (g . p) `1 = (cR * l) . p by A14, EUCLID:56;
B22: cR is continuous by A3, PRE_TOPC:56;
(cR * l) . p in A by A9, A21, SQUARE_1:84, TOPREAL6:20;
then consider Wc being Subset of R^1 such that
A23: p in Wc and
A24: Wc is open and
A25: (cR * l) .: Wc c= A by A20, B22, A1, A4, A5, Th5, JGRAPH_2:20;
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 A17, A23, XBOOLE_0:def 4; :: thesis: ( Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus Ws /\ Wc is open by A18, A24, TOPS_1:38; :: thesis: g .: (Ws /\ Wc) c= V
let y be set ; :: 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
A26: x in Ws /\ Wc and
A27: y = g . x by FUNCT_2:116;
A28: g . x = |[((cR * l) . x),((sR * l) . x)]| by Lm22;
x in Ws by A26, XBOOLE_0:def 4;
then A29: (sR * l) . x in (sR * l) .: Ws by FUNCT_2:43;
x in Wc by A26, XBOOLE_0:def 4;
then A30: (cR * l) . x in (cR * l) .: Wc by FUNCT_2:43;
|[((cR * l) . x),((sR * l) . x)]| = 1,2 --> ((cR * l) . x),((sR * l) . x) by TOPREALA:49;
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 A19, A25, A29, A30, HILBERT3:11;
then |[((cR * l) . x),((sR * l) . x)]| in Ball e,r by A12;
hence y in V by A10, A27, A28; :: thesis: verum

end;

then g is continuous by JGRAPH_2:20;
hence CircleMap is continuous by PRE_TOPC:57; :: thesis: verum