reconsider A = R^1 ].0,1.[ as non empty Subset of R^1 ;
set f = CircleMap ();
set Y = the carrier of (R^1 | A);
reconsider f = CircleMap () as Function of (R^1 | A), by Th32;
reconsider r0 = In (0,REAL) as Point of R^1 by TOPMETR:17;
set F = AffineMap ((2 * PI),0);
A1: dom (id the carrier of (R^1 | A)) = the carrier of (R^1 | A) by RELAT_1:45;
CircleMap . r0 = c by Th32;
then A2: rng f = the carrier of by FUNCT_2:def 3;
A3: the carrier of (R^1 | A) = A by PRE_TOPC:8;
A4: now :: thesis: for a being object st a in dom () holds
() . a = (id the carrier of (R^1 | A)) . a
let a be object ; :: thesis: ( a in dom () implies () . a = (id the carrier of (R^1 | A)) . a )
assume A5: a in dom () ; :: thesis: () . a = (id the carrier of (R^1 | A)) . a
then reconsider b = a as Point of (R^1 | A) ;
reconsider c = b as Element of REAL by XREAL_0:def 1;
consider x, y being Real such that
A6: f . b = |[x,y]| and
A7: ( y >= 0 implies Circle2IntervalR . (f . b) = () / (2 * PI) ) and
A8: ( y <= 0 implies Circle2IntervalR . (f . b) = 1 - (() / (2 * PI)) ) by Def13;
A9: f . b = CircleMap . b by
.= |[((cos * (AffineMap ((2 * PI),0))) . c),((sin * (AffineMap ((2 * PI),0))) . c)]| by Lm20 ;
then y = (sin * (AffineMap ((2 * PI),0))) . c by ;
then A10: y = sin . ((AffineMap ((2 * PI),0)) . c) by FUNCT_2:15;
x = (cos * (AffineMap ((2 * PI),0))) . c by ;
then x = cos . ((AffineMap ((2 * PI),0)) . c) by FUNCT_2:15;
then A11: x = cos ((AffineMap ((2 * PI),0)) . c) by SIN_COS:def 19;
A12: c < 1 by ;
A13: (AffineMap ((2 * PI),0)) . c = ((2 * PI) * c) + 0 by FCONT_1:def 4;
then A14: ((AffineMap ((2 * PI),0)) . c) / ((2 * PI) * 1) = c / 1 by XCMPLX_1:91;
A15: (AffineMap ((2 * PI),0)) . (1 - c) = ((2 * PI) * (1 - c)) + 0 by FCONT_1:def 4;
then A16: ((AffineMap ((2 * PI),0)) . (1 - c)) / ((2 * PI) * 1) = (1 - c) / 1 by XCMPLX_1:91;
A17: now :: thesis: Circle2IntervalR . (f . b) = b
per cases ( y >= 0 or y < 0 ) ;
suppose A18: y >= 0 ; :: thesis: Circle2IntervalR . (f . b) = b
then not (AffineMap ((2 * PI),0)) . c in ].PI,(2 * PI).[ by ;
then ( (AffineMap ((2 * PI),0)) . c <= PI or (AffineMap ((2 * PI),0)) . c >= 2 * PI ) by XXREAL_1:4;
then ( ((AffineMap ((2 * PI),0)) . c) / (2 * PI) <= (1 * PI) / (2 * PI) or ((AffineMap ((2 * PI),0)) . c) / (2 * PI) >= (2 * PI) / (2 * PI) ) by XREAL_1:72;
then c <= 1 / 2 by ;
then A19: (2 * PI) * c <= (2 * PI) * (1 / 2) by XREAL_1:64;
0 <= c by ;
hence Circle2IntervalR . (f . b) = ((AffineMap ((2 * PI),0)) . c) / (2 * PI) by
.= b by ;
:: thesis: verum
end;
suppose A20: y < 0 ; :: thesis: Circle2IntervalR . (f . b) = b
then not (AffineMap ((2 * PI),0)) . c in by ;
then ( (AffineMap ((2 * PI),0)) . c < 0 or (AffineMap ((2 * PI),0)) . c > PI ) by XXREAL_1:1;
then ( ((AffineMap ((2 * PI),0)) . c) / (2 * PI) < 0 / (2 * PI) or ((AffineMap ((2 * PI),0)) . c) / (2 * PI) > (1 * PI) / (2 * PI) ) by XREAL_1:74;
then ( c < 0 or c > 1 / 2 ) by ;
then 1 - c < 1 - (1 / 2) by ;
then A21: (2 * PI) * (1 - c) <= (2 * PI) * (1 / 2) by XREAL_1:64;
A22: 1 - c > 1 - 1 by ;
cos . ((AffineMap ((2 * PI),0)) . (1 - c)) = cos ((- ((2 * PI) * c)) + ((2 * PI) * 1)) by
.= cos (- ((2 * PI) * c)) by COMPLEX2:9
.= cos ((2 * PI) * c) by SIN_COS:31 ;
then arccos x = arccos (cos ((AffineMap ((2 * PI),0)) . (1 - c))) by
.= (AffineMap ((2 * PI),0)) . (1 - c) by ;
hence Circle2IntervalR . (f . b) = b by A8, A16, A20; :: thesis: verum
end;
end;
end;
thus () . a = Circle2IntervalR . (f . b) by
.= (id the carrier of (R^1 | A)) . a by A17 ; :: thesis: verum
end;
dom () = the carrier of (R^1 | A) by FUNCT_2:def 1;
then Circle2IntervalR = f " by ;
hence (CircleMap ()) " = Circle2IntervalR by TOPS_2:def 4; :: thesis: verum