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₁[ Element of NAT ] means sin (x + (((2 * $1) + 1) * PI )) = - (sin x);
A1: S₁[ 0 ] by SIN_COS:84;
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: 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:80
.= - (sin x) by A3, SIN_COS:82 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence sin (x + (((2 * n) + 1) * PI )) = - (sin x) ; :: thesis: verum