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;

(|.sin .| + |.cos .|) . (x + (PI / 2)) = (|.sin .| . (x + (PI / 2))) + (|.cos .| . (x + (PI / 2))) by A2, 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