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 holds Circle2IntervalR is_continuous_at p
proof
Tcircle ((0. ()),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 ; :: thesis:
A2: [.(- 1),1.] = [#] (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18;
reconsider q = p as Point of () 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 = () / (2 * PI) ) and
A6: ( y <= 0 implies Circle2IntervalR . p = 1 - (() / (2 * PI)) ) by Def13;
A7: y = q `2 by ;
A8: x = q `1 by ;
then A9: x <= 1 by Th26;
- 1 <= x by ;
then A10: x in [.(- 1),1.] by ;
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 ;
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 = () * (1 / (2 * PI)) by
.= (1 * ()) / (2 * PI) by XCMPLX_1:74 ;
per cases ( y = 0 or y < 0 or y > 0 ) ;
suppose A15: y < 0 ; :: thesis:
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 st
( W is open & p in W & Circle2IntervalR .: W c= V )
proof
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 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 st
( W is open & p in W & Circle2IntervalR .: W c= V )

reconsider V1 = V as Subset of REAL by ;
reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;
V2 is open by ;
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 ;
A19: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . x = (h1 - ((1 / (2 * PI)) (#) arccos)) . x by ;
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 ;
then A21: dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.] by RELAT_1:62;
A22: Circle2IntervalR . p = 1 - (() / (2 * PI)) by ;
A23: p = (1,2) --> (x,y) by ;
x in dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) by ;
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
.= 1 - ((1 * ()) / (2 * PI)) by ;
then consider N being Neighbourhood of x such that
A25: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1 by ;
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 ;
set W = (product ((1,2) --> (N3,J))) /\ the carrier of ;
reconsider W = (product ((1,2) --> (N3,J))) /\ the carrier of as Subset of 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 ;
R^1 N = N ;
then reconsider M3 = N3 as open Subset of (Closed-Interval-TSpace ((- 1),1)) by ;
KK = product ((1,2) --> (M3,I3)) ;
then KK is open by TOPREALA:39;
hence W is open by ; :: thesis: ( p in W & Circle2IntervalR .: W c= V )
x in N by RCOMP_1:16;
then A28: x in N3 by ;
y >= - 1 by ;
then y in J by ;
then p in product ((1,2) --> (N3,J)) by ;
hence p in W by XBOOLE_0:def 4; :: thesis:
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 such that
A29: c in W and
A30: m = Circle2IntervalR . c by FUNCT_2:65;
A31: c in product ((1,2) --> (N3,J)) by ;
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 ;
then c2 in J by ;
then A35: 1 - ((1 * (arccos c1)) * (1 / (2 * PI))) = m by ;
((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . (c . 1) = (h1 - ((1 / (2 * PI)) (#) arccos)) . (c . 1) by
.= (h1 . (c . 1)) - (((1 / (2 * PI)) (#) arccos) . (c . 1)) by
.= 1 - (((1 / (2 * PI)) (#) arccos) . (c . 1)) by
.= 1 - ((arccos . (c . 1)) * (1 / (2 * PI))) by
.= 1 - ((arccos . c1) * (1 / (2 * PI))) by
.= 1 - ((arccos c1) * (1 / (2 * PI))) by SIN_COS6:def 4 ;
then m in ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 by ;
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;
hence Circle2IntervalR is_continuous_at p by TMAP_1:43; :: thesis: verum
end;
suppose A36: y > 0 ; :: thesis:
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 st
( W is open & p in W & Circle2IntervalR .: W c= V )
proof
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 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 st
( W is open & p in W & Circle2IntervalR .: W c= V )

reconsider V1 = V as Subset of REAL by ;
reconsider V2 = V1 as Subset of R^1 by TOPMETR:17;
V2 is open by ;
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 ;
Circle2IntervalR . p = () / (2 * PI) by ;
then consider N being Neighbourhood of x such that
A40: (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N c= N1 by ;
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 ;
set W = (product ((1,2) --> (N3,I))) /\ the carrier of ;
reconsider W = (product ((1,2) --> (N3,I))) /\ the carrier of as Subset of 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 ;
R^1 N = N ;
then reconsider M3 = N3 as open Subset of (Closed-Interval-TSpace ((- 1),1)) by ;
KK = product ((1,2) --> (M3,I3)) ;
then KK is open by TOPREALA:39;
hence W is open by ; :: thesis: ( p in W & Circle2IntervalR .: W c= V )
x in N by RCOMP_1:16;
then A43: x in N3 by ;
A44: dom (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) = [.(- 1),1.] by ;
A45: p = (1,2) --> (x,y) by ;
y <= 1 by ;
then y in I by ;
then p in product ((1,2) --> (N3,I)) by ;
hence p in W by XBOOLE_0:def 4; :: thesis:
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 such that
A46: c in W and
A47: m = Circle2IntervalR . c by FUNCT_2:65;
A48: c in product ((1,2) --> (N3,I)) by ;
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 ;
then c2 in I by ;
then A52: (1 * (arccos c1)) * (1 / (2 * PI)) = m by ;
(((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) . (c . 1) = ((1 / (2 * PI)) (#) arccos) . (c . 1) by
.= (arccos . (c . 1)) * (1 / (2 * PI)) by
.= (arccos . c1) * (1 / (2 * PI)) by
.= (arccos c1) * (1 / (2 * PI)) by SIN_COS6:def 4 ;
then m in (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N3 by ;
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;
hence Circle2IntervalR is_continuous_at p by TMAP_1:43; :: thesis: verum
end;
end;
end;
hence Circle2IntervalR is continuous by TMAP_1:44; :: thesis: verum