for x being Real 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; :: 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:24, 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, XREAL_0:def 1
.= |.(sin . (x + (PI / 2))).| + (|.cos.| . (x + (PI / 2))) by A2, VALUED_1:def 11, XREAL_0:def 1
.= |.(sin . (x + (PI / 2))).| + |.(cos . (x + (PI / 2))).| by A2, VALUED_1:def 11, XREAL_0:def 1
.= |.(cos . x).| + |.(cos . (x + (PI / 2))).| by SIN_COS:78
.= |.(cos . x).| + |.(- (sin . x)).| by SIN_COS:78
.= |.(cos . x).| + |.(sin . x).| by COMPLEX1:52
.= (|.cos.| . x) + |.(sin . x).| by A1, A2, VALUED_1:def 11
.= (|.cos.| . x) + (|.sin.| . x) by A1, A2, VALUED_1:def 11
.= (|.sin.| + |.cos.|) . x by A1, VALUED_1:def 1 ;
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, XREAL_0:def 1; :: thesis: verum

end;

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