for x being real number st x in dom (sin (#) cos ) holds
( x + PI in dom (sin (#) cos ) & x - PI in dom (sin (#) cos ) & (sin (#) cos ) . x = (sin (#) cos ) . (x + PI ) )

proof

let x be real number ; :: thesis: ( x in dom (sin (#) cos ) implies ( x + PI in dom (sin (#) cos ) & x - PI in dom (sin (#) cos ) & (sin (#) cos ) . x = (sin (#) cos ) . (x + PI ) ) )
assume A1: x in dom (sin (#) cos ) ; :: thesis: ( x + PI in dom (sin (#) cos ) & x - PI in dom (sin (#) cos ) & (sin (#) cos ) . x = (sin (#) cos ) . (x + PI ) )
A2: ( x + PI in (dom sin ) /\ (dom cos ) & x - PI in (dom sin ) /\ (dom cos ) ) by SIN_COS:27;
then ( x + PI in dom (sin (#) cos ) & x - PI in dom (sin (#) cos ) ) by VALUED_1:def 4;
then (sin (#) cos ) . (x + PI ) = (sin . (x + PI )) * (cos . (x + PI )) by VALUED_1:def 4
.= (- (sin . x)) * (cos . (x + PI )) by SIN_COS:83
.= (- (sin . x)) * (- (cos . x)) by SIN_COS:83
.= (sin . x) * (cos . x)
.= (sin (#) cos ) . x by A1, VALUED_1:def 4 ;
hence ( x + PI in dom (sin (#) cos ) & x - PI in dom (sin (#) cos ) & (sin (#) cos ) . x = (sin (#) cos ) . (x + PI ) ) by A2, VALUED_1:def 4; :: thesis: verum

end;

hence sin (#) cos is PI -periodic by Th1; :: thesis: verum