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

proof

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

end;

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