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) )

( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) )

proof

hence
cos ^2 is PI -periodic
by Th1; :: thesis: verum
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;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