let a, b be Real; :: thesis: b + (a (#) sin) is 2 * PI -periodic
for x being Real 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; :: 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 A1: x in dom (a (#) sin) by SIN_COS:24, VALUED_1:def 5;
then A2: ( 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:24, XREAL_0:def 1;
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 A3, VALUED_1:def 5
.= b + (a * (sin . x)) by SIN_COS:78
.= b + ((a (#) sin) . x) by A1, VALUED_1:def 5
.= (b + (a (#) sin)) . x by A2, VALUED_1:def 2 ;
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