reconsider A1 = R^1 ].(1 / 2),((1 / 2) + p1).[ as non empty Subset of R^1 ;
set f = CircleMap (R^1 (1 / 2));
set Y = the carrier of (R^1 | A1);
reconsider f = CircleMap (R^1 (1 / 2)) as Function of (R^1 | A1), by Lm19;
set G = AffineMap ((2 * PI),0);
A1: dom (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) = the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by RELAT_1:45;
A2: rng f = the carrier of by ;
A3: the carrier of (R^1 | A1) = A1 by PRE_TOPC:8;
A4: now :: thesis: for a being object st a in dom () holds
() . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a
let a be object ; :: thesis: ( a in dom () implies () . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a )
assume A5: a in dom () ; :: thesis: () . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a
then reconsider b = a as Point of (R^1 | A1) ;
reconsider c = b as Real ;
consider x, y being Real such that
A6: f . b = |[x,y]| and
A7: ( y >= 0 implies Circle2IntervalL . (f . b) = 1 + (() / (2 * PI)) ) and
A8: ( y <= 0 implies Circle2IntervalL . (f . b) = 1 - (() / (2 * PI)) ) by Def14;
A9: f . b = CircleMap . b by
.= |[(cos ((2 * PI) * c)),(sin ((2 * PI) * c))]| by Def11 ;
then A10: y = sin ((2 * PI) * c) by ;
A11: 1 / 2 < c by ;
then (2 * PI) * (1 / 2) < (2 * PI) * c by XREAL_1:68;
then A12: PI + ((2 * PI) * 0) < (2 * PI) * c ;
A13: c < 3 / 2 by ;
then c - 1 < (3 / 2) - 1 by XREAL_1:9;
then A14: (2 * PI) * (c - 1) <= (2 * PI) * (1 / 2) by XREAL_1:64;
(2 * PI) * c <= (2 * PI) * ((1 / 2) + 1) by ;
then A15: (2 * PI) * c <= PI + ((2 * PI) * 1) ;
A16: (AffineMap ((2 * PI),0)) . (1 - c) = ((2 * PI) * (1 - c)) + 0 by FCONT_1:def 4;
then A17: ((AffineMap ((2 * PI),0)) . (1 - c)) / ((2 * PI) * 1) = (1 - c) / 1 by XCMPLX_1:91;
A18: x = cos ((2 * PI) * c) by
.= cos (((2 * PI) * c) + ((2 * PI) * (- 1))) by COMPLEX2:9
.= cos ((2 * PI) * (c - 1)) ;
A19: now :: thesis: Circle2IntervalL . (f . b) = b
per cases ( c >= 1 or c < 1 ) ;
suppose A20: c >= 1 ; :: thesis: Circle2IntervalL . (f . b) = b
then A21: 1 - 1 <= c - 1 by XREAL_1:9;
(2 * PI) * c >= (2 * PI) * 1 by ;
hence Circle2IntervalL . (f . b) = 1 + (((2 * PI) * (c - 1)) / (2 * PI)) by
.= 1 + (c - 1) by XCMPLX_1:89
.= b ;
:: thesis: verum
end;
suppose A22: c < 1 ; :: thesis: Circle2IntervalL . (f . b) = b
then (2 * PI) * c < (2 * PI) * 1 by XREAL_1:68;
then A23: (2 * PI) * c < (2 * PI) + ((2 * PI) * 0) ;
1 - c < 1 - (1 / 2) by ;
then A24: (2 * PI) * (1 - c) <= (2 * PI) * (1 / 2) by XREAL_1:64;
A25: 1 - 1 <= 1 - c by ;
arccos x = arccos (cos ((2 * PI) * c)) by
.= arccos (cos (- ((2 * PI) * c))) by SIN_COS:31
.= arccos (cos (((2 * PI) * (- c)) + ((2 * PI) * 1))) by COMPLEX2:9
.= (AffineMap ((2 * PI),0)) . (1 - c) by ;
hence Circle2IntervalL . (f . b) = b by ; :: thesis: verum
end;
end;
end;
thus () . a = Circle2IntervalL . (f . b) by
.= (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a by A19 ; :: thesis: verum
end;
dom () = the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by FUNCT_2:def 1;
then Circle2IntervalL = f " by ;
hence (CircleMap (R^1 (1 / 2))) " = Circle2IntervalL by TOPS_2:def 4; :: thesis: verum