reconsider c1 = c[-10] as Point of () ;
let aX1 be Subset of ; :: thesis: ( aX1 = { q where q is Point of () : ( q in the carrier of & 0 >= q `2 ) } implies Circle2IntervalR | ( | aX1) is continuous )
assume A1: aX1 = { q where q is Point of () : ( q in the carrier of & 0 >= q `2 ) } ; :: thesis:
A2: c1 `2 = 0 by EUCLID:52;
c[-10] is Point of by ;
then c[-10] in aX1 by A1, A2;
then reconsider aX1 = aX1 as non empty Subset of ;
set X1 = | aX1;
A3: the carrier of () is Subset of () by TSEP_1:1;
[#] ( | aX1) is Subset of () by Lm9;
then reconsider B = [#] ( | aX1) as non empty Subset of () by ;
set f = p | B;
A4: dom (p | B) = B by ;
A5: aX1 = the carrier of ( | aX1) by PRE_TOPC:8;
A6: rng (p | B) c= Q
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p | B) or y in Q )
assume y in rng (p | B) ; :: thesis: y in Q
then consider x being object such that
A7: x in dom (p | B) and
A8: (p | B) . x = y by FUNCT_1:def 3;
consider q being Point of () such that
A9: q = x and
A10: q in the carrier of and
0 >= q `2 by A1, A5, A4, A7;
A11: - 1 <= q `1 by ;
A12: q `1 < 1 by ;
y = p . x by
.= q `1 by ;
hence y in Q by ; :: thesis: verum
end;
A13: the carrier of (() | B) = B by PRE_TOPC:8;
then reconsider f = p | B as Function of (() | B),(R^1 | (R^1 Q)) by ;
(Topen_unit_circle c[10]) | aX1 is SubSpace of Tunit_circle 2 by TSEP_1:7;
then (Topen_unit_circle c[10]) | aX1 is SubSpace of TOP-REAL 2 by TSEP_1:7;
then A14: (TOP-REAL 2) | B = | aX1 by PRE_TOPC:def 5;
A15: for a being Point of ( | aX1) holds (Circle2IntervalR | ( | aX1)) . a = (L * (Af * (c * f))) . a
proof
let a be Point of ( | aX1); :: thesis: (Circle2IntervalR | ( | aX1)) . a = (L * (Af * (c * f))) . a
reconsider b = a as Point of by PRE_TOPC:25;
consider x, y being Real such that
A16: b = |[x,y]| and
( y >= 0 implies Circle2IntervalR . b = () / (2 * PI) ) and
A17: ( y <= 0 implies Circle2IntervalR . b = 1 - (() / (2 * PI)) ) by Def13;
A18: |[x,y]| `1 < 1 by ;
dom (Af * (c * f)) = the carrier of (() | B) by FUNCT_2:def 1;
then A19: (Af * (c * f)) . a in rng (Af * (c * f)) by ;
reconsider r = (Af * (c * f)) . a as Real ;
a in aX1 by A5;
then A20: ex q being Point of () st
( a = q & q in the carrier of & 0 >= q `2 ) by A1;
A21: |[x,y]| `1 = x by EUCLID:52;
- 1 <= |[x,y]| `1 by ;
then A22: x in Q by ;
then arccos . x = c . x by FUNCT_1:49;
then A23: arccos . x in rng c by ;
() / (2 * PI) = () / (2 * PI) by SIN_COS6:def 4
.= ((1 / (2 * PI)) * ()) + 0 by XCMPLX_1:99
.= (AffineMap ((1 / (2 * PI)),0)) . () by FCONT_1:def 4
.= Af . () by
.= Af . (c . x) by
.= Af . (c . (|[x,y]| `1)) by EUCLID:52
.= Af . (c . (p . a)) by
.= Af . (c . (f . a)) by FUNCT_1:49
.= Af . ((c * f) . a) by
.= (Af * (c * f)) . a by ;
hence (Circle2IntervalR | ( | aX1)) . a = ((- 1) * r) + 1 by
.= (R^1 (AffineMap ((- 1),1))) . r by FCONT_1:def 4
.= L . r by
.= (L * (Af * (c * f))) . a by ;
:: thesis: verum
end;
f is continuous by ;
hence Circle2IntervalR | ( | aX1) is continuous by ; :: thesis: verum