let x be Real; :: thesis: for n being Element of NAT holds sin (x + (((2 * n) + 1) * PI)) = - (sin x)
let n be Element of NAT ; :: thesis: sin (x + (((2 * n) + 1) * PI)) = - (sin x)
defpred S₁[ Nat] means sin (x + (((2 * $1) + 1) * PI)) = - (sin x);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: sin (x + (((2 * n) + 1) * PI)) = - (sin x) ; :: thesis: S₁[n + 1]
sin (x + (((2 * (n + 1)) + 1) * PI)) = sin ((x + (((2 * n) + 1) * PI)) + (2 * PI))
.= ((sin (x + (((2 * n) + 1) * PI))) * (cos (2 * PI))) + ((cos (x + (((2 * n) + 1) * PI))) * (sin (2 * PI))) by SIN_COS:75
.= - (sin x) by A2, SIN_COS:77 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ] by SIN_COS:79;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence sin (x + (((2 * n) + 1) * PI)) = - (sin x) ; :: thesis: verum