theorem :: FUNCT_9:29

for i being non zero Integer holds |.sin.| + |.cos.| is (PI / 2) * i -periodic