defpred S₁[ Nat] means sin . ($1 * PI) = 0 ;
A1: S₁[ 0 ] by SIN_COS:30;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
sin . ((n + 1) * PI) = sin . ((n * PI) + PI)
.= (0 * (cos . PI)) + ((cos . (n * PI)) * (sin . PI)) by SIN_COS:74, A3
.= 0 by SIN_COS:77 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence for n being Nat holds sin . (n * PI) = 0 ; :: thesis: verum