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

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

set J = [.p0,0.[;

set I = ].0,p1.];

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

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

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

set J = [.p0,0.[;

set I = ].0,p1.];

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

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

proof

hence
Circle2IntervalR 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: Circle2IntervalR 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 ].0,(0 + p1).[)) = ].0,(0 + p1).[ by PRE_TOPC:8;

consider x, y being Real such that

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

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

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

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;

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

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

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

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

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

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

then A14: ((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: Circle2IntervalR 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 ].0,(0 + p1).[)) = ].0,(0 + p1).[ by PRE_TOPC:8;

consider x, y being Real such that

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

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

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

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;

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

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

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

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

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

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

then A14: ((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 A15:
y < 0
; :: thesis: Circle2IntervalR is_continuous_at p

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

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

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

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

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

proof

hence
Circle2IntervalR 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 ].0,(0 + p1).[)); :: thesis: ( V is open & Circle2IntervalR . p in V implies ex W being Subset of (Topen_unit_circle c[10]) st

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

assume that

A16: V is open and

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

( W is open & p in W & Circle2IntervalR .: 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 A16, TSEP_1:17;

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

consider N1 being Neighbourhood of Circle2IntervalR . p such that

A18: N1 c= V1 by A17, RCOMP_1:18;

A19: ((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 A20: dom (h1 - ((1 / (2 * PI)) (#) arccos)) = REAL /\ (dom ((1 / (2 * PI)) (#) arccos))

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

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

A22: Circle2IntervalR . p = 1 - ((arccos . x) / (2 * PI)) by A6, A15, SIN_COS6:def 4;

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

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

then A24: (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, A20, VALUED_1:13

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

then consider N being Neighbourhood of x such that

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

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

A26: 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 & Circle2IntervalR .: 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;

A27: ((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, Lm16, TOPS_2:24; :: thesis: ( p in W & Circle2IntervalR .: W c= V )

x in N by RCOMP_1:16;

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

y >= - 1 by A7, Th26;

then y in J by A15, XXREAL_1:3;

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

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

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

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

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

A29: c in W and

A30: m = Circle2IntervalR . c by FUNCT_2:65;

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

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

consider c1, c2 being Real such that

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

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

A34: ( c2 <= 0 implies Circle2IntervalR . c = 1 - ((arccos c1) / (2 * PI)) ) by Def13;

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

then c2 in J by A33, TOPREALA:29;

then A35: 1 - ((1 * (arccos c1)) * (1 / (2 * PI))) = m by A30, A34, XCMPLX_1:74, XXREAL_1:3;

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

.= (h1 . (c . 1)) - (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A20, A26, A32, VALUED_1:13

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

.= 1 - ((arccos . (c . 1)) * (1 / (2 * PI))) by A13, A26, A32, SIN_COS6:86, VALUED_1:def 5

.= 1 - ((arccos . c1) * (1 / (2 * PI))) by A33, 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 A26, A32, A21, A35, FUNCT_1:def 6;

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

then m in N1 by A25;

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

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

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

assume that

A16: V is open and

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

( W is open & p in W & Circle2IntervalR .: 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 A16, TSEP_1:17;

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

consider N1 being Neighbourhood of Circle2IntervalR . p such that

A18: N1 c= V1 by A17, RCOMP_1:18;

A19: ((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 A20: dom (h1 - ((1 / (2 * PI)) (#) arccos)) = REAL /\ (dom ((1 / (2 * PI)) (#) arccos))

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

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

A22: Circle2IntervalR . p = 1 - ((arccos . x) / (2 * PI)) by A6, A15, SIN_COS6:def 4;

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

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

then A24: (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, A20, VALUED_1:13

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

then consider N being Neighbourhood of x such that

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

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

A26: 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 & Circle2IntervalR .: 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;

A27: ((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, Lm16, TOPS_2:24; :: thesis: ( p in W & Circle2IntervalR .: W c= V )

x in N by RCOMP_1:16;

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

y >= - 1 by A7, Th26;

then y in J by A15, XXREAL_1:3;

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

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

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

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

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

A29: c in W and

A30: m = Circle2IntervalR . c by FUNCT_2:65;

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

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

consider c1, c2 being Real such that

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

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

A34: ( c2 <= 0 implies Circle2IntervalR . c = 1 - ((arccos c1) / (2 * PI)) ) by Def13;

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

then c2 in J by A33, TOPREALA:29;

then A35: 1 - ((1 * (arccos c1)) * (1 / (2 * PI))) = m by A30, A34, XCMPLX_1:74, XXREAL_1:3;

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

.= (h1 . (c . 1)) - (((1 / (2 * PI)) (#) arccos) . (c . 1)) by A20, A26, A32, VALUED_1:13

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

.= 1 - ((arccos . (c . 1)) * (1 / (2 * PI))) by A13, A26, A32, SIN_COS6:86, VALUED_1:def 5

.= 1 - ((arccos . c1) * (1 / (2 * PI))) by A33, 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 A26, A32, A21, A35, FUNCT_1:def 6;

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

then m in N1 by A25;

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

suppose A36:
y > 0
; :: thesis: Circle2IntervalR is_continuous_at p

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

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

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

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

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

proof

hence
Circle2IntervalR is_continuous_at p
by TMAP_1:43; :: thesis: verum
let V be Subset of (R^1 | (R^1 ].0,(0 + p1).[)); :: thesis: ( V is open & Circle2IntervalR . p in V implies ex W being Subset of (Topen_unit_circle c[10]) st

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

assume that

A37: V is open and

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

( W is open & p in W & Circle2IntervalR .: 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 A37, TSEP_1:17;

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

consider N1 being Neighbourhood of Circle2IntervalR . p such that

A39: N1 c= V1 by A38, RCOMP_1:18;

Circle2IntervalR . p = (arccos . x) / (2 * PI) by A5, A36, SIN_COS6:def 4;

then consider N being Neighbourhood of x such that

A40: (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N c= N1 by A11, A14, A12, FCONT_1:5;

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

A41: 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 & Circle2IntervalR .: 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;

A42: (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N3 c= (((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, Lm16, TOPS_2:24; :: thesis: ( p in W & Circle2IntervalR .: W c= V )

x in N by RCOMP_1:16;

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

A44: dom (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) = [.(- 1),1.] by A13, RELAT_1:62, SIN_COS6:86;

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

y <= 1 by A7, Th26;

then y in I by A36, XXREAL_1:2;

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

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

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

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

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

A46: c in W and

A47: m = Circle2IntervalR . c by FUNCT_2:65;

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

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

consider c1, c2 being Real such that

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

A51: ( c2 >= 0 implies Circle2IntervalR . c = (arccos c1) / (2 * PI) ) and

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

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

then c2 in I by A50, TOPREALA:29;

then A52: (1 * (arccos c1)) * (1 / (2 * PI)) = m by A47, A51, XCMPLX_1:74, XXREAL_1:2;

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

.= (arccos . (c . 1)) * (1 / (2 * PI)) by A13, A41, A49, SIN_COS6:86, VALUED_1:def 5

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

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

then m in (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N3 by A41, A49, A44, A52, FUNCT_1:def 6;

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

then m in N1 by A40;

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

end;( W is open & p in W & Circle2IntervalR .: W c= V ) )

assume that

A37: V is open and

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

( W is open & p in W & Circle2IntervalR .: 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 A37, TSEP_1:17;

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

consider N1 being Neighbourhood of Circle2IntervalR . p such that

A39: N1 c= V1 by A38, RCOMP_1:18;

Circle2IntervalR . p = (arccos . x) / (2 * PI) by A5, A36, SIN_COS6:def 4;

then consider N being Neighbourhood of x such that

A40: (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N c= N1 by A11, A14, A12, FCONT_1:5;

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

A41: 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 & Circle2IntervalR .: 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;

A42: (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N3 c= (((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, Lm16, TOPS_2:24; :: thesis: ( p in W & Circle2IntervalR .: W c= V )

x in N by RCOMP_1:16;

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

A44: dom (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) = [.(- 1),1.] by A13, RELAT_1:62, SIN_COS6:86;

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

y <= 1 by A7, Th26;

then y in I by A36, XXREAL_1:2;

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

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

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

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

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

A46: c in W and

A47: m = Circle2IntervalR . c by FUNCT_2:65;

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

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

consider c1, c2 being Real such that

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

A51: ( c2 >= 0 implies Circle2IntervalR . c = (arccos c1) / (2 * PI) ) and

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

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

then c2 in I by A50, TOPREALA:29;

then A52: (1 * (arccos c1)) * (1 / (2 * PI)) = m by A47, A51, XCMPLX_1:74, XXREAL_1:2;

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

.= (arccos . (c . 1)) * (1 / (2 * PI)) by A13, A41, A49, SIN_COS6:86, VALUED_1:def 5

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

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

then m in (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N3 by A41, A49, A44, A52, FUNCT_1:def 6;

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

then m in N1 by A40;

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