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

proof

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

end;

hence sin ^2 is PI -periodic by Th1; :: thesis: verum