reconsider c1 = c 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 Circle2IntervalL | ( | 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 is Point of by ;
then c 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;
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 A13: (TOP-REAL 2) | B = | aX1 by PRE_TOPC:def 5;
A14: for a being Point of ( | aX1) holds () . a = (Af * (c * f)) . a
proof
let a be Point of ( | aX1); :: thesis: () . a = (Af * (c * f)) . a
reconsider b = a as Point of by PRE_TOPC:25;
consider x, y being Real such that
A15: b = |[x,y]| and
( y >= 0 implies Circle2IntervalL . b = 1 + (() / (2 * PI)) ) and
A16: ( y <= 0 implies Circle2IntervalL . b = 1 - (() / (2 * PI)) ) by Def14;
A17: |[x,y]| `1 <= 1 by ;
A18: |[x,y]| `1 = x by EUCLID:52;
- 1 < |[x,y]| `1 by ;
then A19: x in Q by ;
then arccos . x = c . x by FUNCT_1:49;
then A20: arccos . x in rng c by ;
a in aX1 by A5;
then ex q being Point of () st
( a = q & q in the carrier of & 0 >= q `2 ) by A1;
hence () . a = 1 - (() / (2 * PI)) by
.= 1 - (() / (2 * PI)) by SIN_COS6:def 4
.= 1 - ((1 / (2 * PI)) * ()) by XCMPLX_1:99
.= ((- (1 / (2 * PI))) * ()) + 1
.= (AffineMap ((- (1 / (2 * PI))),1)) . () 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 ;
:: thesis: verum
end;
f is continuous by ;
hence Circle2IntervalL | ( | aX1) is continuous by ; :: thesis: verum