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 holds Circle2IntervalL 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 ].(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 + (() / (2 * PI)) ) and
A6: ( y <= 0 implies Circle2IntervalL . p = 1 - (() / (2 * PI)) ) by Def14;
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 ;
A11: dom ((1 / (2 * PI)) (#) arccos) = dom arccos by VALUED_1:def 5;
then A12: ((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 A13: y < 0 ; :: thesis:
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 st
( W is open & p in W & Circle2IntervalL .: W c= V )
proof
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 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 st
( W is open & p in W & Circle2IntervalL .: 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 Circle2IntervalL . p such that
A16: N1 c= V1 by ;
A17: ((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 A18: dom (h1 - ((1 / (2 * PI)) (#) arccos)) = REAL /\ (dom ((1 / (2 * PI)) (#) arccos))
.= [.(- 1),1.] by ;
then A19: dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.] by RELAT_1:62;
A20: Circle2IntervalL . p = 1 - (() / (2 * PI)) by ;
A21: p = (1,2) --> (x,y) by ;
x in dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) by ;
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
.= 1 - ((1 * ()) / (2 * PI)) by ;
then consider N being Neighbourhood of x such that
A23: ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1 by ;
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 ;
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 & 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 ;
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 & Circle2IntervalL .: W c= V )
x in N by RCOMP_1:16;
then A26: 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 Circle2IntervalL .: W or m in V )
assume m in Circle2IntervalL .: W ; :: thesis: m in V
then consider c being Element of such that
A27: c in W and
A28: m = Circle2IntervalL . c by FUNCT_2:65;
A29: c in product ((1,2) --> (N3,J)) by ;
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 ;
then c2 in J by ;
then A33: 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 A25;
then m in N1 by A23;
hence m in V by A16; :: thesis: verum
end;
hence Circle2IntervalL is_continuous_at p by TMAP_1:43; :: thesis: verum
end;
suppose A34: y > 0 ; :: thesis:
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 st
( W is open & p in W & Circle2IntervalL .: W c= V )
proof
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 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 st
( W is open & p in W & Circle2IntervalL .: 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 Circle2IntervalL . p such that
A37: N1 c= V1 by ;
A38: ((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:def 1;
then A39: dom (h1 + ((1 / (2 * PI)) (#) arccos)) = REAL /\ (dom ((1 / (2 * PI)) (#) arccos))
.= [.(- 1),1.] by ;
then A40: dom ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.] by RELAT_1:62;
A41: Circle2IntervalL . p = 1 + (() / (2 * PI)) by ;
A42: p = (1,2) --> (x,y) by ;
x in dom ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) by ;
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
.= 1 + ((1 * ()) / (2 * PI)) by ;
then consider N being Neighbourhood of x such that
A44: ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1 by ;
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 ;
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 & 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 ;
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 & Circle2IntervalL .: W c= V )
x in N by RCOMP_1:16;
then A47: x in N3 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 Circle2IntervalL .: W or m in V )
assume m in Circle2IntervalL .: W ; :: thesis: m in V
then consider c being Element of such that
A48: c in W and
A49: m = Circle2IntervalL . c by FUNCT_2:65;
A50: c in product ((1,2) --> (N3,I)) by ;
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 ;
then c2 in I by ;
then A54: 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 A46;
then m in N1 by A44;
hence m in V by A37; :: thesis: verum
end;
hence Circle2IntervalL is_continuous_at p by TMAP_1:43; :: thesis: verum
end;
end;
end;
hence Circle2IntervalL is continuous by TMAP_1:44; :: thesis: verum