let r be real number ; :: thesis: for i being Integer holds sin r = sin (((2 * PI ) * i) + r)
let i be Integer; :: thesis: sin r = sin (((2 * PI ) * i) + r)
A1: sin . r = sin r by SIN_COS:def 21;
A2: sin . (((2 * PI ) * i) + r) = sin (((2 * PI ) * i) + r) by SIN_COS:def 21;
A3: sin . (((2 * PI ) * (- i)) + (((2 * PI ) * i) + r)) = sin (((2 * PI ) * (- i)) + (((2 * PI ) * i) + r)) by SIN_COS:def 21;

per cases ( i >= 0 or i < 0 ) ;

suppose i >= 0 ; :: thesis: sin r = sin (((2 * PI ) * i) + r)

then reconsider iN = i as Element of NAT by INT_1:16;
sin r = sin (((2 * PI ) * iN) + r) by A1, A2, SIN_COS2:10;
hence sin r = sin (((2 * PI ) * i) + r) ; :: thesis: verum

end;

suppose i < 0 ; :: thesis: sin r = sin (((2 * PI ) * i) + r)

then reconsider iN = - i as Element of NAT by INT_1:16;
reconsider aa = ((2 * PI ) * i) + r as Real ;
sin aa = sin (((2 * PI ) * iN) + aa) by A2, A3, SIN_COS2:10;
hence sin r = sin (((2 * PI ) * i) + r) ; :: thesis: verum

end;

end;