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;