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

proof

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

end;

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