let r, s be real number ; :: thesis: for i being integer number st (2 * PI ) * i <= r & r < (2 * PI ) + ((2 * PI ) * i) & (2 * PI ) * i <= s & s < (2 * PI ) + ((2 * PI ) * i) & sin r = sin s & cos r = cos s holds
r = s
let i be integer number ; :: thesis: ( (2 * PI ) * i <= r & r < (2 * PI ) + ((2 * PI ) * i) & (2 * PI ) * i <= s & s < (2 * PI ) + ((2 * PI ) * i) & sin r = sin s & cos r = cos s implies r = s )
assume that
A1: (2 * PI ) * i <= r and
A2: r < (2 * PI ) + ((2 * PI ) * i) and
A3: (2 * PI ) * i <= s and
A4: s < (2 * PI ) + ((2 * PI ) * i) and
A5: sin r = sin s and
A6: cos r = cos s ; :: thesis: r = s
A7: cos (r - s) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by COMPLEX2:4
.= 1 by A5, A6, SIN_COS:32 ;
A8: cos (s - r) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by COMPLEX2:4
.= 1 by A5, A6, SIN_COS:32 ;
A9: sin (r - s) = ((sin r) * (cos s)) - ((cos r) * (sin s)) by COMPLEX2:4
.= 0 by A5, A6 ;
A10: sin (s - r) = ((sin s) * (cos r)) - ((cos s) * (sin r)) by COMPLEX2:4
.= 0 by A5, A6 ;

per cases ( r > s or r < s or r = s ) by XXREAL_0:1;

suppose r > s ; :: thesis: r = s

then r > s + 0 ;
then A11: 0 <= r - s by XREAL_1:22;
r + ((2 * PI ) * i) < ((2 * PI ) + ((2 * PI ) * i)) + s by A2, A3, XREAL_1:10;
then (r + ((2 * PI ) * i)) - ((2 * PI ) * i) < (((2 * PI ) + ((2 * PI ) * i)) + s) - ((2 * PI ) * i) by XREAL_1:11;
then r < (2 * PI ) + s ;
then r - s < 2 * PI by XREAL_1:21;
then ( r - s = 0 or r - s = PI ) by A9, A11, COMPTRIG:33;
hence r = s by A7, SIN_COS:82; :: thesis: verum

end;

suppose r < s ; :: thesis: r = s

then s > r + 0 ;
then A12: 0 <= s - r by XREAL_1:22;
s + ((2 * PI ) * i) < ((2 * PI ) + ((2 * PI ) * i)) + r by A1, A4, XREAL_1:10;
then (s + ((2 * PI ) * i)) - ((2 * PI ) * i) < (((2 * PI ) + ((2 * PI ) * i)) + r) - ((2 * PI ) * i) by XREAL_1:11;
then s < (2 * PI ) + r ;
then s - r < 2 * PI by XREAL_1:21;
then ( s - r = 0 or s - r = PI ) by A10, A12, COMPTRIG:33;
hence r = s by A8, SIN_COS:82; :: thesis: verum

end;

suppose r = s ; :: thesis: r = s

hence r = s ; :: thesis: verum

end;

end;