set h = (1 / (2 * PI)) (#) arccos;

set K = [.(- 1),1.];

set J = [.p0,0.[;

set I = ].0,p1.];

set Z = R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[);

for p being Point of (Topen_unit_circle c[-10]) holds Circle2IntervalL is_continuous_at p

set K = [.(- 1),1.];

set J = [.p0,0.[;

set I = ].0,p1.];

set Z = R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[);

for p being Point of (Topen_unit_circle c[-10]) holds Circle2IntervalL is_continuous_at p

proof

hence
Circle2IntervalL is continuous
by TMAP_1:44; :: thesis: verum
Tcircle ((0. (TOP-REAL 2)),1) is SubSpace of Trectangle (p0,p1,p0,p1)
by Th10;

then A1: Topen_unit_circle c[-10] is SubSpace of Trectangle (p0,p1,p0,p1) by TSEP_1:7;

let p be Point of (Topen_unit_circle c[-10]); :: thesis: Circle2IntervalL is_continuous_at p

A2: [.(- 1),1.] = [#] (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18;

reconsider q = p as Point of (TOP-REAL 2) by Lm8;

A3: the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) = ].(1 / 2),((1 / 2) + p1).[ by PRE_TOPC:8;

consider x, y being Real such that

A4: p = |[x,y]| and

A5: ( y >= 0 implies Circle2IntervalL . p = 1 + ((arccos x) / (2 * PI)) ) and

A6: ( y <= 0 implies Circle2IntervalL . p = 1 - ((arccos x) / (2 * PI)) ) by Def14;

A7: y = q `2 by A4, EUCLID:52;

A8: x = q `1 by A4, EUCLID:52;

then A9: x <= 1 by Th26;

- 1 <= x by A8, Th26;

then A10: x in [.(- 1),1.] by A9, XXREAL_1:1;

A11: dom ((1 / (2 * PI)) (#) arccos) = dom arccos by VALUED_1:def 5;

then A12: ((1 / (2 * PI)) (#) arccos) . x = (arccos . x) * (1 / (2 * PI)) by A10, SIN_COS6:86, VALUED_1:def 5

.= (1 * (arccos . x)) / (2 * PI) by XCMPLX_1:74 ;

end;then A1: Topen_unit_circle c[-10] is SubSpace of Trectangle (p0,p1,p0,p1) by TSEP_1:7;

let p be Point of (Topen_unit_circle c[-10]); :: thesis: Circle2IntervalL is_continuous_at p

A2: [.(- 1),1.] = [#] (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18;

reconsider q = p as Point of (TOP-REAL 2) by Lm8;

A3: the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) = ].(1 / 2),((1 / 2) + p1).[ by PRE_TOPC:8;

consider x, y being Real such that

A4: p = |[x,y]| and

A5: ( y >= 0 implies Circle2IntervalL . p = 1 + ((arccos x) / (2 * PI)) ) and

A6: ( y <= 0 implies Circle2IntervalL . p = 1 - ((arccos x) / (2 * PI)) ) by Def14;

A7: y = q `2 by A4, EUCLID:52;

A8: x = q `1 by A4, EUCLID:52;

then A9: x <= 1 by Th26;

- 1 <= x by A8, Th26;

then A10: x in [.(- 1),1.] by A9, XXREAL_1:1;

A11: dom ((1 / (2 * PI)) (#) arccos) = dom arccos by VALUED_1:def 5;

then A12: ((1 / (2 * PI)) (#) arccos) . x = (arccos . x) * (1 / (2 * PI)) by A10, SIN_COS6:86, VALUED_1:def 5

.= (1 * (arccos . x)) / (2 * PI) by XCMPLX_1:74 ;

per cases
( y = 0 or y < 0 or y > 0 )
;

end;

suppose A13:
y < 0
; :: thesis: Circle2IntervalL is_continuous_at p

for V being Subset of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) st V is open & Circle2IntervalL . p in V holds

ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V )

end;ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V )

proof

hence
Circle2IntervalL is_continuous_at p
by TMAP_1:43; :: thesis: verum
set hh = h1 - ((1 / (2 * PI)) (#) arccos);

let V be Subset of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)); :: thesis: ( V is open & Circle2IntervalL . p in V implies ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V ) )

assume that

A14: V is open and

A15: Circle2IntervalL . p in V ; :: thesis: ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V )

reconsider V1 = V as Subset of REAL by A3, XBOOLE_1:1;

reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;

V2 is open by A14, TSEP_1:17;

then reconsider V1 = V1 as open Subset of REAL by BORSUK_5:39;

consider N1 being Neighbourhood of Circle2IntervalL . p such that

A16: N1 c= V1 by A15, RCOMP_1:18;

A17: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . x = (h1 - ((1 / (2 * PI)) (#) arccos)) . x by A10, FUNCT_1:49;

dom (h1 - ((1 / (2 * PI)) (#) arccos)) = (dom h1) /\ (dom ((1 / (2 * PI)) (#) arccos)) by VALUED_1:12;

then A18: dom (h1 - ((1 / (2 * PI)) (#) arccos)) = REAL /\ (dom ((1 / (2 * PI)) (#) arccos))

.= [.(- 1),1.] by A11, SIN_COS6:86, XBOOLE_1:28 ;

then A19: dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.] by RELAT_1:62;

A20: Circle2IntervalL . p = 1 - ((arccos . x) / (2 * PI)) by A6, A13, SIN_COS6:def 4;

A21: p = (1,2) --> (x,y) by A4, TOPREALA:28;

x in dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) by A10, A18, RELAT_1:57;

then A22: (h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.] is_continuous_in x by FCONT_1:def 2;

(h1 - ((1 / (2 * PI)) (#) arccos)) . x = (h1 . x) - (((1 / (2 * PI)) (#) arccos) . x) by A10, A18, VALUED_1:13

.= 1 - ((1 * (arccos . x)) / (2 * PI)) by A10, A12, FUNCOP_1:7 ;

then consider N being Neighbourhood of x such that

A23: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1 by A20, A17, A22, FCONT_1:5;

set N3 = N /\ [.(- 1),1.];

A24: N /\ [.(- 1),1.] c= [.(- 1),1.] by XBOOLE_1:17;

reconsider N3 = N /\ [.(- 1),1.], J = [.p0,0.[ as Subset of (Closed-Interval-TSpace ((- 1),1)) by Lm2, XBOOLE_1:17, XXREAL_1:35;

set W = (product ((1,2) --> (N3,J))) /\ the carrier of (Topen_unit_circle c[-10]);

reconsider W = (product ((1,2) --> (N3,J))) /\ the carrier of (Topen_unit_circle c[-10]) as Subset of (Topen_unit_circle c[-10]) by XBOOLE_1:17;

take W ; :: thesis: ( W is open & p in W & Circle2IntervalL .: W c= V )

reconsider KK = product ((1,2) --> (N3,J)) as Subset of (Trectangle (p0,p1,p0,p1)) by TOPREALA:38;

reconsider I3 = J as open Subset of (Closed-Interval-TSpace ((- 1),1)) by TOPREALA:26;

A25: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 c= ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N by RELAT_1:123, XBOOLE_1:17;

R^1 N = N ;

then reconsider M3 = N3 as open Subset of (Closed-Interval-TSpace ((- 1),1)) by A2, TOPS_2:24;

KK = product ((1,2) --> (M3,I3)) ;

then KK is open by TOPREALA:39;

hence W is open by A1, Lm17, TOPS_2:24; :: thesis: ( p in W & Circle2IntervalL .: W c= V )

x in N by RCOMP_1:16;

then A26: x in N3 by A10, XBOOLE_0:def 4;

y >= - 1 by A7, Th26;

then y in J by A13, XXREAL_1:3;

then p in product ((1,2) --> (N3,J)) by A21, A26, HILBERT3:11;

hence p in W by XBOOLE_0:def 4; :: thesis: Circle2IntervalL .: W c= V

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in Circle2IntervalL .: W or m in V )

assume m in Circle2IntervalL .: W ; :: thesis: m in V

then consider c being Element of (Topen_unit_circle c[-10]) such that

A27: c in W and

A28: m = Circle2IntervalL . c by FUNCT_2:65;

A29: c in product ((1,2) --> (N3,J)) by A27, XBOOLE_0:def 4;

then A30: c . 1 in N3 by TOPREALA:3;

consider c1, c2 being Real such that

A31: c = |[c1,c2]| and

( c2 >= 0 implies Circle2IntervalL . c = 1 + ((arccos c1) / (2 * PI)) ) and

A32: ( c2 <= 0 implies Circle2IntervalL . c = 1 - ((arccos c1) / (2 * PI)) ) by Def14;

c . 2 in J by A29, TOPREALA:3;

then c2 in J by A31, TOPREALA:29;

then A33: 1 - ((1 * (arccos c1)) * (1 / (2 * PI))) = m by A28, A32, XCMPLX_1:74, XXREAL_1:3;

((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . (c . 1) = (h1 - ((1 / (2 * PI)) (#) arccos)) . (c . 1) by A24, A30, FUNCT_1:49

.= (h1 . (c . 1)) - (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A18, A24, A30, VALUED_1:13

.= 1 - (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A30, FUNCOP_1:7

.= 1 - ((arccos . (c . 1)) * (1 / (2 * PI))) by A11, A24, A30, SIN_COS6:86, VALUED_1:def 5

.= 1 - ((arccos . c1) * (1 / (2 * PI))) by A31, TOPREALA:29

.= 1 - ((arccos c1) * (1 / (2 * PI))) by SIN_COS6:def 4 ;

then m in ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 by A24, A30, A19, A33, FUNCT_1:def 6;

then m in ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N by A25;

then m in N1 by A23;

hence m in V by A16; :: thesis: verum

end;let V be Subset of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)); :: thesis: ( V is open & Circle2IntervalL . p in V implies ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V ) )

assume that

A14: V is open and

A15: Circle2IntervalL . p in V ; :: thesis: ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V )

reconsider V1 = V as Subset of REAL by A3, XBOOLE_1:1;

reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;

V2 is open by A14, TSEP_1:17;

then reconsider V1 = V1 as open Subset of REAL by BORSUK_5:39;

consider N1 being Neighbourhood of Circle2IntervalL . p such that

A16: N1 c= V1 by A15, RCOMP_1:18;

A17: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . x = (h1 - ((1 / (2 * PI)) (#) arccos)) . x by A10, FUNCT_1:49;

dom (h1 - ((1 / (2 * PI)) (#) arccos)) = (dom h1) /\ (dom ((1 / (2 * PI)) (#) arccos)) by VALUED_1:12;

then A18: dom (h1 - ((1 / (2 * PI)) (#) arccos)) = REAL /\ (dom ((1 / (2 * PI)) (#) arccos))

.= [.(- 1),1.] by A11, SIN_COS6:86, XBOOLE_1:28 ;

then A19: dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.] by RELAT_1:62;

A20: Circle2IntervalL . p = 1 - ((arccos . x) / (2 * PI)) by A6, A13, SIN_COS6:def 4;

A21: p = (1,2) --> (x,y) by A4, TOPREALA:28;

x in dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) by A10, A18, RELAT_1:57;

then A22: (h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.] is_continuous_in x by FCONT_1:def 2;

(h1 - ((1 / (2 * PI)) (#) arccos)) . x = (h1 . x) - (((1 / (2 * PI)) (#) arccos) . x) by A10, A18, VALUED_1:13

.= 1 - ((1 * (arccos . x)) / (2 * PI)) by A10, A12, FUNCOP_1:7 ;

then consider N being Neighbourhood of x such that

A23: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1 by A20, A17, A22, FCONT_1:5;

set N3 = N /\ [.(- 1),1.];

A24: N /\ [.(- 1),1.] c= [.(- 1),1.] by XBOOLE_1:17;

reconsider N3 = N /\ [.(- 1),1.], J = [.p0,0.[ as Subset of (Closed-Interval-TSpace ((- 1),1)) by Lm2, XBOOLE_1:17, XXREAL_1:35;

set W = (product ((1,2) --> (N3,J))) /\ the carrier of (Topen_unit_circle c[-10]);

reconsider W = (product ((1,2) --> (N3,J))) /\ the carrier of (Topen_unit_circle c[-10]) as Subset of (Topen_unit_circle c[-10]) by XBOOLE_1:17;

take W ; :: thesis: ( W is open & p in W & Circle2IntervalL .: W c= V )

reconsider KK = product ((1,2) --> (N3,J)) as Subset of (Trectangle (p0,p1,p0,p1)) by TOPREALA:38;

reconsider I3 = J as open Subset of (Closed-Interval-TSpace ((- 1),1)) by TOPREALA:26;

A25: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 c= ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N by RELAT_1:123, XBOOLE_1:17;

R^1 N = N ;

then reconsider M3 = N3 as open Subset of (Closed-Interval-TSpace ((- 1),1)) by A2, TOPS_2:24;

KK = product ((1,2) --> (M3,I3)) ;

then KK is open by TOPREALA:39;

hence W is open by A1, Lm17, TOPS_2:24; :: thesis: ( p in W & Circle2IntervalL .: W c= V )

x in N by RCOMP_1:16;

then A26: x in N3 by A10, XBOOLE_0:def 4;

y >= - 1 by A7, Th26;

then y in J by A13, XXREAL_1:3;

then p in product ((1,2) --> (N3,J)) by A21, A26, HILBERT3:11;

hence p in W by XBOOLE_0:def 4; :: thesis: Circle2IntervalL .: W c= V

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in Circle2IntervalL .: W or m in V )

assume m in Circle2IntervalL .: W ; :: thesis: m in V

then consider c being Element of (Topen_unit_circle c[-10]) such that

A27: c in W and

A28: m = Circle2IntervalL . c by FUNCT_2:65;

A29: c in product ((1,2) --> (N3,J)) by A27, XBOOLE_0:def 4;

then A30: c . 1 in N3 by TOPREALA:3;

consider c1, c2 being Real such that

A31: c = |[c1,c2]| and

( c2 >= 0 implies Circle2IntervalL . c = 1 + ((arccos c1) / (2 * PI)) ) and

A32: ( c2 <= 0 implies Circle2IntervalL . c = 1 - ((arccos c1) / (2 * PI)) ) by Def14;

c . 2 in J by A29, TOPREALA:3;

then c2 in J by A31, TOPREALA:29;

then A33: 1 - ((1 * (arccos c1)) * (1 / (2 * PI))) = m by A28, A32, XCMPLX_1:74, XXREAL_1:3;

((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . (c . 1) = (h1 - ((1 / (2 * PI)) (#) arccos)) . (c . 1) by A24, A30, FUNCT_1:49

.= (h1 . (c . 1)) - (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A18, A24, A30, VALUED_1:13

.= 1 - (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A30, FUNCOP_1:7

.= 1 - ((arccos . (c . 1)) * (1 / (2 * PI))) by A11, A24, A30, SIN_COS6:86, VALUED_1:def 5

.= 1 - ((arccos . c1) * (1 / (2 * PI))) by A31, TOPREALA:29

.= 1 - ((arccos c1) * (1 / (2 * PI))) by SIN_COS6:def 4 ;

then m in ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 by A24, A30, A19, A33, FUNCT_1:def 6;

then m in ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N by A25;

then m in N1 by A23;

hence m in V by A16; :: thesis: verum

suppose A34:
y > 0
; :: thesis: Circle2IntervalL is_continuous_at p

for V being Subset of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) st V is open & Circle2IntervalL . p in V holds

ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V )

end;ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V )

proof

hence
Circle2IntervalL is_continuous_at p
by TMAP_1:43; :: thesis: verum
set hh = h1 + ((1 / (2 * PI)) (#) arccos);

let V be Subset of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)); :: thesis: ( V is open & Circle2IntervalL . p in V implies ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V ) )

assume that

A35: V is open and

A36: Circle2IntervalL . p in V ; :: thesis: ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V )

reconsider V1 = V as Subset of REAL by A3, XBOOLE_1:1;

reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;

V2 is open by A35, TSEP_1:17;

then reconsider V1 = V1 as open Subset of REAL by BORSUK_5:39;

consider N1 being Neighbourhood of Circle2IntervalL . p such that

A37: N1 c= V1 by A36, RCOMP_1:18;

A38: ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . x = (h1 + ((1 / (2 * PI)) (#) arccos)) . x by A10, FUNCT_1:49;

dom (h1 + ((1 / (2 * PI)) (#) arccos)) = (dom h1) /\ (dom ((1 / (2 * PI)) (#) arccos)) by VALUED_1:def 1;

then A39: dom (h1 + ((1 / (2 * PI)) (#) arccos)) = REAL /\ (dom ((1 / (2 * PI)) (#) arccos))

.= [.(- 1),1.] by A11, SIN_COS6:86, XBOOLE_1:28 ;

then A40: dom ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.] by RELAT_1:62;

A41: Circle2IntervalL . p = 1 + ((arccos . x) / (2 * PI)) by A5, A34, SIN_COS6:def 4;

A42: p = (1,2) --> (x,y) by A4, TOPREALA:28;

x in dom ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) by A10, A39, RELAT_1:57;

then A43: (h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.] is_continuous_in x by FCONT_1:def 2;

(h1 + ((1 / (2 * PI)) (#) arccos)) . x = (h1 . x) + (((1 / (2 * PI)) (#) arccos) . x) by A10, A39, VALUED_1:def 1

.= 1 + ((1 * (arccos . x)) / (2 * PI)) by A10, A12, FUNCOP_1:7 ;

then consider N being Neighbourhood of x such that

A44: ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1 by A41, A38, A43, FCONT_1:5;

set N3 = N /\ [.(- 1),1.];

A45: N /\ [.(- 1),1.] c= [.(- 1),1.] by XBOOLE_1:17;

reconsider N3 = N /\ [.(- 1),1.], I = ].0,p1.] as Subset of (Closed-Interval-TSpace ((- 1),1)) by Lm2, XBOOLE_1:17, XXREAL_1:36;

set W = (product ((1,2) --> (N3,I))) /\ the carrier of (Topen_unit_circle c[-10]);

reconsider W = (product ((1,2) --> (N3,I))) /\ the carrier of (Topen_unit_circle c[-10]) as Subset of (Topen_unit_circle c[-10]) by XBOOLE_1:17;

take W ; :: thesis: ( W is open & p in W & Circle2IntervalL .: W c= V )

reconsider KK = product ((1,2) --> (N3,I)) as Subset of (Trectangle (p0,p1,p0,p1)) by TOPREALA:38;

reconsider I3 = I as open Subset of (Closed-Interval-TSpace ((- 1),1)) by TOPREALA:25;

A46: ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 c= ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N by RELAT_1:123, XBOOLE_1:17;

R^1 N = N ;

then reconsider M3 = N3 as open Subset of (Closed-Interval-TSpace ((- 1),1)) by A2, TOPS_2:24;

KK = product ((1,2) --> (M3,I3)) ;

then KK is open by TOPREALA:39;

hence W is open by A1, Lm17, TOPS_2:24; :: thesis: ( p in W & Circle2IntervalL .: W c= V )

x in N by RCOMP_1:16;

then A47: x in N3 by A10, XBOOLE_0:def 4;

y <= 1 by A7, Th26;

then y in I by A34, XXREAL_1:2;

then p in product ((1,2) --> (N3,I)) by A42, A47, HILBERT3:11;

hence p in W by XBOOLE_0:def 4; :: thesis: Circle2IntervalL .: W c= V

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in Circle2IntervalL .: W or m in V )

assume m in Circle2IntervalL .: W ; :: thesis: m in V

then consider c being Element of (Topen_unit_circle c[-10]) such that

A48: c in W and

A49: m = Circle2IntervalL . c by FUNCT_2:65;

A50: c in product ((1,2) --> (N3,I)) by A48, XBOOLE_0:def 4;

then A51: c . 1 in N3 by TOPREALA:3;

consider c1, c2 being Real such that

A52: c = |[c1,c2]| and

A53: ( c2 >= 0 implies Circle2IntervalL . c = 1 + ((arccos c1) / (2 * PI)) ) and

( c2 <= 0 implies Circle2IntervalL . c = 1 - ((arccos c1) / (2 * PI)) ) by Def14;

c . 2 in I by A50, TOPREALA:3;

then c2 in I by A52, TOPREALA:29;

then A54: 1 + ((1 * (arccos c1)) * (1 / (2 * PI))) = m by A49, A53, XCMPLX_1:74, XXREAL_1:2;

((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . (c . 1) = (h1 + ((1 / (2 * PI)) (#) arccos)) . (c . 1) by A45, A51, FUNCT_1:49

.= (h1 . (c . 1)) + (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A39, A45, A51, VALUED_1:def 1

.= 1 + (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A51, FUNCOP_1:7

.= 1 + ((arccos . (c . 1)) * (1 / (2 * PI))) by A11, A45, A51, SIN_COS6:86, VALUED_1:def 5

.= 1 + ((arccos . c1) * (1 / (2 * PI))) by A52, TOPREALA:29

.= 1 + ((arccos c1) * (1 / (2 * PI))) by SIN_COS6:def 4 ;

then m in ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 by A45, A51, A40, A54, FUNCT_1:def 6;

then m in ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N by A46;

then m in N1 by A44;

hence m in V by A37; :: thesis: verum

end;let V be Subset of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)); :: thesis: ( V is open & Circle2IntervalL . p in V implies ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V ) )

assume that

A35: V is open and

A36: Circle2IntervalL . p in V ; :: thesis: ex W being Subset of (Topen_unit_circle c[-10]) st

( W is open & p in W & Circle2IntervalL .: W c= V )

reconsider V1 = V as Subset of REAL by A3, XBOOLE_1:1;

reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;

V2 is open by A35, TSEP_1:17;

then reconsider V1 = V1 as open Subset of REAL by BORSUK_5:39;

consider N1 being Neighbourhood of Circle2IntervalL . p such that

A37: N1 c= V1 by A36, RCOMP_1:18;

A38: ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . x = (h1 + ((1 / (2 * PI)) (#) arccos)) . x by A10, FUNCT_1:49;

dom (h1 + ((1 / (2 * PI)) (#) arccos)) = (dom h1) /\ (dom ((1 / (2 * PI)) (#) arccos)) by VALUED_1:def 1;

then A39: dom (h1 + ((1 / (2 * PI)) (#) arccos)) = REAL /\ (dom ((1 / (2 * PI)) (#) arccos))

.= [.(- 1),1.] by A11, SIN_COS6:86, XBOOLE_1:28 ;

then A40: dom ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.] by RELAT_1:62;

A41: Circle2IntervalL . p = 1 + ((arccos . x) / (2 * PI)) by A5, A34, SIN_COS6:def 4;

A42: p = (1,2) --> (x,y) by A4, TOPREALA:28;

x in dom ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) by A10, A39, RELAT_1:57;

then A43: (h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.] is_continuous_in x by FCONT_1:def 2;

(h1 + ((1 / (2 * PI)) (#) arccos)) . x = (h1 . x) + (((1 / (2 * PI)) (#) arccos) . x) by A10, A39, VALUED_1:def 1

.= 1 + ((1 * (arccos . x)) / (2 * PI)) by A10, A12, FUNCOP_1:7 ;

then consider N being Neighbourhood of x such that

A44: ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1 by A41, A38, A43, FCONT_1:5;

set N3 = N /\ [.(- 1),1.];

A45: N /\ [.(- 1),1.] c= [.(- 1),1.] by XBOOLE_1:17;

reconsider N3 = N /\ [.(- 1),1.], I = ].0,p1.] as Subset of (Closed-Interval-TSpace ((- 1),1)) by Lm2, XBOOLE_1:17, XXREAL_1:36;

set W = (product ((1,2) --> (N3,I))) /\ the carrier of (Topen_unit_circle c[-10]);

reconsider W = (product ((1,2) --> (N3,I))) /\ the carrier of (Topen_unit_circle c[-10]) as Subset of (Topen_unit_circle c[-10]) by XBOOLE_1:17;

take W ; :: thesis: ( W is open & p in W & Circle2IntervalL .: W c= V )

reconsider KK = product ((1,2) --> (N3,I)) as Subset of (Trectangle (p0,p1,p0,p1)) by TOPREALA:38;

reconsider I3 = I as open Subset of (Closed-Interval-TSpace ((- 1),1)) by TOPREALA:25;

A46: ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 c= ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N by RELAT_1:123, XBOOLE_1:17;

R^1 N = N ;

then reconsider M3 = N3 as open Subset of (Closed-Interval-TSpace ((- 1),1)) by A2, TOPS_2:24;

KK = product ((1,2) --> (M3,I3)) ;

then KK is open by TOPREALA:39;

hence W is open by A1, Lm17, TOPS_2:24; :: thesis: ( p in W & Circle2IntervalL .: W c= V )

x in N by RCOMP_1:16;

then A47: x in N3 by A10, XBOOLE_0:def 4;

y <= 1 by A7, Th26;

then y in I by A34, XXREAL_1:2;

then p in product ((1,2) --> (N3,I)) by A42, A47, HILBERT3:11;

hence p in W by XBOOLE_0:def 4; :: thesis: Circle2IntervalL .: W c= V

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in Circle2IntervalL .: W or m in V )

assume m in Circle2IntervalL .: W ; :: thesis: m in V

then consider c being Element of (Topen_unit_circle c[-10]) such that

A48: c in W and

A49: m = Circle2IntervalL . c by FUNCT_2:65;

A50: c in product ((1,2) --> (N3,I)) by A48, XBOOLE_0:def 4;

then A51: c . 1 in N3 by TOPREALA:3;

consider c1, c2 being Real such that

A52: c = |[c1,c2]| and

A53: ( c2 >= 0 implies Circle2IntervalL . c = 1 + ((arccos c1) / (2 * PI)) ) and

( c2 <= 0 implies Circle2IntervalL . c = 1 - ((arccos c1) / (2 * PI)) ) by Def14;

c . 2 in I by A50, TOPREALA:3;

then c2 in I by A52, TOPREALA:29;

then A54: 1 + ((1 * (arccos c1)) * (1 / (2 * PI))) = m by A49, A53, XCMPLX_1:74, XXREAL_1:2;

((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . (c . 1) = (h1 + ((1 / (2 * PI)) (#) arccos)) . (c . 1) by A45, A51, FUNCT_1:49

.= (h1 . (c . 1)) + (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A39, A45, A51, VALUED_1:def 1

.= 1 + (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A51, FUNCOP_1:7

.= 1 + ((arccos . (c . 1)) * (1 / (2 * PI))) by A11, A45, A51, SIN_COS6:86, VALUED_1:def 5

.= 1 + ((arccos . c1) * (1 / (2 * PI))) by A52, TOPREALA:29

.= 1 + ((arccos c1) * (1 / (2 * PI))) by SIN_COS6:def 4 ;

then m in ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 by A45, A51, A40, A54, FUNCT_1:def 6;

then m in ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N by A46;

then m in N1 by A44;

hence m in V by A37; :: thesis: verum