for x being real number 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 number ; :: 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:27;
then A3: ( x + PI in dom |.cos .| & x - PI in dom |.cos .| ) by VALUED_1:def 11;
|.cos .| . (x + PI ) = |.(cos (x + PI )).| by A3, VALUED_1:def 11
.= |.(- (cos . x)).| by SIN_COS:83
.= |.(cos . x).| by COMPLEX1:138
.= |.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