for x being Real st x in dom |.sin.| holds
( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) )

proof

let x be Real; :: thesis: ( x in dom |.sin.| implies ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) ) )
assume A1: x in dom |.sin.| ; :: thesis: ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) )
A2: ( x + PI in dom sin & x - PI in dom sin ) by SIN_COS:24, XREAL_0:def 1;
then ( x + PI in dom |.sin.| & x - PI in dom |.sin.| ) by VALUED_1:def 11;
then |.sin.| . (x + PI) = |.(sin (x + PI)).| by VALUED_1:def 11
.= |.(- (sin . x)).| by SIN_COS:78
.= |.(sin . x).| by COMPLEX1:52
.= |.sin.| . x by A1, VALUED_1:def 11 ;
hence ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) ) by A2, VALUED_1:def 11; :: thesis: verum

end;

hence |.sin.| is PI -periodic by Th1; :: thesis: verum