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

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

proof

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