for x being real number 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 number ; :: 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:27;
then A3: ( x + PI in dom |.sin .| & x - PI in dom |.sin .| ) by VALUED_1:def 11;
|.sin .| . (x + PI ) = |.(sin (x + PI )).| by A3, VALUED_1:def 11
.= |.(- (sin . x)).| by SIN_COS:83
.= |.(sin . x).| by COMPLEX1:138
.= |.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