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;
( 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.|)
;
( 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 )
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;
verum
end;
hence
|.sin.| + |.cos.| is PI / 2 -periodic
by Th1; verum