let th be Real; :: thesis: for n being Nat holds sin . th = sin . (((2 * PI) * n) + th)
defpred S₁[ Nat] means for th being Real holds sin . th = sin . (((2 * PI) * $1) + th);
let n be Nat; :: thesis: sin . th = sin . (((2 * PI) * n) + th)
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: for th being Real holds sin . th = sin . (((2 * PI) * n) + th) ; :: thesis: S₁[n + 1]
for th being Real holds sin . th = sin . (((2 * PI) * (n + 1)) + th)

proof

let th be Real; :: thesis: sin . th = sin . (((2 * PI) * (n + 1)) + th)
sin . (((2 * PI) * (n + 1)) + th) = sin . ((((2 * PI) * n) + th) + (2 * PI))
.= sin . (((2 * PI) * n) + th) by SIN_COS:78
.= sin . th by A2 ;
hence sin . th = sin . (((2 * PI) * (n + 1)) + th) ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

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