for x being real number st x in dom (|.sin.| + |.cos.|) holds
( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) )

proof

let x be real number ; :: thesis: ( x in dom (|.sin.| + |.cos.|) implies ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) ) )
assume A1: x in dom (|.sin.| + |.cos.|) ; :: thesis: ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) )
A2: ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL )

proof

A3: dom (|.sin.| + |.cos.|) = (dom |.sin.|) /\ (dom |.cos.|) by VALUED_1:def 1;
( dom |.sin.| = REAL & dom |.cos.| = REAL ) by SIN_COS:27, VALUED_1:def 11;
hence ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL ) by A3; :: thesis: verum

end;

then (|.sin.| + |.cos.|) . (x + (PI / 2)) = (|.sin.| . (x + (PI / 2))) + (|.cos.| . (x + (PI / 2))) by VALUED_1:def 1
.= |.(sin . (x + (PI / 2))).| + (|.cos.| . (x + (PI / 2))) by VALUED_1:def 11, A2
.= |.(sin . (x + (PI / 2))).| + |.(cos . (x + (PI / 2))).| by VALUED_1:def 11, A2
.= |.(cos . x).| + |.(cos . (x + (PI / 2))).| by SIN_COS:83
.= |.(cos . x).| + |.(- (sin . x)).| by SIN_COS:83
.= |.(cos . x).| + |.(sin . x).| by COMPLEX1:138
.= (|.cos.| . x) + |.(sin . x).| by VALUED_1:def 11, A1, A2
.= (|.cos.| . x) + (|.sin.| . x) by VALUED_1:def 11, A1, A2
.= (|.sin.| + |.cos.|) . x by VALUED_1:def 1, A1 ;
hence ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) ) by A2; :: thesis: verum

end;

hence |.sin.| + |.cos.| is PI / 2 -periodic by Th1; :: thesis: verum