let r, s be Real; :: thesis: ( sin r = sin s & cos r = cos s implies ex i being Integer st r = s + ((2 * PI) * i) )
assume that
A1: sin r = sin s and
A2: cos r = cos s ; :: thesis: ex i being Integer st r = s + ((2 * PI) * i)
consider i being Integer such that
A3: ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) by A1, Th9;
consider j being Integer such that
A4: ( r = s + ((2 * PI) * j) or r = (- s) + ((2 * PI) * j) ) by A2, Th10;

per cases ( r = s + ((2 * PI) * i) or r = s + ((2 * PI) * j) or ( r = (PI - s) + ((2 * PI) * i) & r = (- s) + ((2 * PI) * j) ) ) by A3, A4;

suppose ( r = s + ((2 * PI) * i) or r = s + ((2 * PI) * j) ) ; :: thesis: ex i being Integer st r = s + ((2 * PI) * i)

hence ex i being Integer st r = s + ((2 * PI) * i) ; :: thesis: verum

end;

suppose ( r = (PI - s) + ((2 * PI) * i) & r = (- s) + ((2 * PI) * j) ) ; :: thesis: ex i being Integer st r = s + ((2 * PI) * i)

then PI / PI = (PI * (2 * (j - i))) / PI ;
then PI / PI = 2 * (j - i) by XCMPLX_1:89;
then 1 = 2 * (j - i) by XCMPLX_1:60;
then j - i = 1 / 2 ;
hence ex i being Integer st r = s + ((2 * PI) * i) by NAT_D:33; :: thesis: verum

end;

end;