for x being Real 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; :: 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:24, XREAL_0:def 1;
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:78
.= (- (sin . x)) * (- (cos . x)) by SIN_COS:78
.= (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