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

proof

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

end;

hence |.cos.| is PI -periodic by Th1; :: thesis: verum