let a, b be Real; :: thesis: b + () is 2 * PI -periodic
for x being Real st x in dom (b + ()) holds
( x + (2 * PI) in dom (b + ()) & x - (2 * PI) in dom (b + ()) & (b + ()) . x = (b + ()) . (x + (2 * PI)) )
proof
let x be Real; :: thesis: ( x in dom (b + ()) implies ( x + (2 * PI) in dom (b + ()) & x - (2 * PI) in dom (b + ()) & (b + ()) . x = (b + ()) . (x + (2 * PI)) ) )
assume x in dom (b + ()) ; :: thesis: ( x + (2 * PI) in dom (b + ()) & x - (2 * PI) in dom (b + ()) & (b + ()) . x = (b + ()) . (x + (2 * PI)) )
x in REAL by XREAL_0:def 1;
then A1: x in dom () by ;
then A2: ( x in dom (b + ()) & x in dom (b + ()) ) by VALUED_1:def 2;
( x + (2 * PI) in dom sin & x - (2 * PI) in dom sin ) by ;
then A3: ( x + (2 * PI) in dom () & x - (2 * PI) in dom () ) by VALUED_1:def 5;
then ( x + (2 * PI) in dom (b + ()) & x - (2 * PI) in dom (b + ()) ) by VALUED_1:def 2;
then (b + ()) . (x + (2 * PI)) = b + (() . (x + (2 * PI))) by VALUED_1:def 2
.= b + (a * (sin . (x + (2 * PI)))) by
.= b + (a * (sin . x)) by SIN_COS:78
.= b + (() . x) by
.= (b + ()) . x by ;
hence ( x + (2 * PI) in dom (b + ()) & x - (2 * PI) in dom (b + ()) & (b + ()) . x = (b + ()) . (x + (2 * PI)) ) by ; :: thesis: verum
end;
hence b + () is 2 * PI -periodic by Th1; :: thesis: verum