let r, s be real number ; :: thesis: ( 0 <= r & r < 2 * PI & 0 <= s & s < 2 * PI & sin r = sin s & cos r = cos s implies r = s )
assume that
A1: 0 <= r and
A2: r < 2 * PI and
A3: 0 <= s and
A4: s < 2 * PI 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 Th4
.= 1 by A5, A6, SIN_COS:32 ;
A8: cos (s - r) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by Th4
.= 1 by A5, A6, SIN_COS:32 ;
A9: sin (r - s) = ((sin r) * (cos s)) - ((cos r) * (sin s)) by Th4
.= 0 by A5, A6 ;
A10: sin (s - r) = ((sin s) * (cos r)) - ((cos s) * (sin r)) by Th4
.= 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 + 0 < (2 * PI ) + s by A2, A3, XREAL_1:10;
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 + 0 < (2 * PI ) + r by A1, A4, XREAL_1:10;
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;