let r, s be Real; :: 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 & 0 <= s ) and
A3: s < 2 * PI and
A4: ( sin r = sin s & cos r = cos s ) ; :: thesis: r = s
A5: cos (r - s) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by Th3
.= 1 by A4, SIN_COS:29 ;
A6: sin (r - s) = ((sin r) * (cos s)) - ((cos r) * (sin s)) by Th3
.= 0 by A4 ;
A7: cos (s - r) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by Th3
.= 1 by A4, SIN_COS:29 ;
A8: sin (s - r) = ((sin s) * (cos r)) - ((cos s) * (sin r)) by Th3
.= 0 by A4 ;

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

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

r + 0 < (2 * PI) + s by A2, XREAL_1:8;
then A10: r - s < 2 * PI by XREAL_1:19;
r > s + 0 by A9;
then 0 <= r - s by XREAL_1:20;
then ( r - s = 0 or r - s = PI ) by A6, A10, COMPTRIG:17;
hence r = s by A5, SIN_COS:77; :: thesis: verum

end;

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

then s > r + 0 ;
then A11: 0 <= s - r by XREAL_1:20;
s + 0 < (2 * PI) + r by A1, A3, XREAL_1:8;
then s - r < 2 * PI by XREAL_1:19;
then ( s - r = 0 or s - r = PI ) by A8, A11, COMPTRIG:17;
hence r = s by A7, SIN_COS:77; :: thesis: verum

end;

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

hence r = s ; :: thesis: verum

end;

end;