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

proof

let th be real number ; :: thesis: cos . th = cos . (((2 * PI ) * (n + 1)) + th)
cos . (((2 * PI ) * (n + 1)) + th) = cos . ((((2 * PI ) * n) + th) + (2 * PI ))
.= cos . (((2 * PI ) * n) + th) by SIN_COS:83
.= cos . th by A3 ;
hence cos . th = cos . (((2 * PI ) * (n + 1)) + th) ; :: thesis: verum

end;

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

end;

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