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 )

hence CircleMap is continuous by PRE_TOPC:27; :: thesis: verum

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

then
g is continuous
by JGRAPH_2:10;
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;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

hence CircleMap is continuous by PRE_TOPC:27; :: thesis: verum