let b, a be real number ; :: thesis: b + (a (#) cos ) is 2 * PI -periodic
for x being real number st x in dom (b + (a (#) cos )) holds
( x + (2 * PI ) in dom (b + (a (#) cos )) & x - (2 * PI ) in dom (b + (a (#) cos )) & (b + (a (#) cos )) . x = (b + (a (#) cos )) . (x + (2 * PI )) )

proof

let x be real number ; :: thesis: ( x in dom (b + (a (#) cos )) implies ( x + (2 * PI ) in dom (b + (a (#) cos )) & x - (2 * PI ) in dom (b + (a (#) cos )) & (b + (a (#) cos )) . x = (b + (a (#) cos )) . (x + (2 * PI )) ) )
assume x in dom (b + (a (#) cos )) ; :: thesis: ( x + (2 * PI ) in dom (b + (a (#) cos )) & x - (2 * PI ) in dom (b + (a (#) cos )) & (b + (a (#) cos )) . x = (b + (a (#) cos )) . (x + (2 * PI )) )
x in REAL by XREAL_0:def 1;
then A0: x in dom (a (#) cos ) by SIN_COS:27, VALUED_1:def 5;
then A1: ( x in dom (b + (a (#) cos )) & x in dom (b + (a (#) cos )) ) by VALUED_1:def 2;
( x + (2 * PI ) in dom cos & x - (2 * PI ) in dom cos ) by SIN_COS:27;
then A3: ( x + (2 * PI ) in dom (a (#) cos ) & x - (2 * PI ) in dom (a (#) cos ) ) by VALUED_1:def 5;
then ( x + (2 * PI ) in dom (b + (a (#) cos )) & x - (2 * PI ) in dom (b + (a (#) cos )) ) by VALUED_1:def 2;
then (b + (a (#) cos )) . (x + (2 * PI )) = b + ((a (#) cos ) . (x + (2 * PI ))) by VALUED_1:def 2
.= b + (a * (cos . (x + (2 * PI )))) by VALUED_1:def 5, A3
.= b + (a * (cos . x)) by SIN_COS:83
.= b + ((a (#) cos ) . x) by VALUED_1:def 5, A0
.= (b + (a (#) cos )) . x by VALUED_1:def 2, A1 ;
hence ( x + (2 * PI ) in dom (b + (a (#) cos )) & x - (2 * PI ) in dom (b + (a (#) cos )) & (b + (a (#) cos )) . x = (b + (a (#) cos )) . (x + (2 * PI )) ) by A3, VALUED_1:def 2; :: thesis: verum

end;

hence b + (a (#) cos ) is 2 * PI -periodic by Th1; :: thesis: verum