let b, a be real number ; :: thesis: for i being non zero Integer holds b + (a (#) cos) is (2 * PI) * i -periodic
let i be non zero Integer; :: thesis: b + (a (#) cos) is (2 * PI) * i -periodic
i in INT by INT_1:def 2;
then consider k being Element of NAT such that
a1: ( i = k or i = - k ) by INT_1:def 1;

per cases ( i = k or i = - k ) by a1;

suppose i = k ; :: thesis: b + (a (#) cos) is (2 * PI) * i -periodic

then ex m being Nat st i = m + 1 by NAT_1:6;
hence b + (a (#) cos) is (2 * PI) * i -periodic by Th36; :: thesis: verum

end;

suppose a2: i = - k ; :: thesis: b + (a (#) cos) is (2 * PI) * i -periodic

then consider m being Nat such that
a3: - i = m + 1 by NAT_1:6;
b + (a (#) cos) is (2 * PI) * (m + 1) -periodic by Th36;
then b + (a (#) cos) is - ((2 * PI) * (m + 1)) -periodic by Th14;
hence b + (a (#) cos) is (2 * PI) * i -periodic by a2, a3; :: thesis: verum

end;

end;