begin
:: deftheorem Def1 defines -periodic FUNCT_9:def 1 :
:: deftheorem Def2 defines periodic FUNCT_9:def 2 :
theorem Th1:
theorem
theorem
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th83:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
L1:
sin is 2 * PI -periodic
begin
L2:
cos is 2 * PI -periodic
theorem
theorem
L3:
cosec is 2 * PI -periodic
L4:
sec is 2 * PI -periodic
theorem
theorem
L5:
tan is PI -periodic
L6:
cot is PI -periodic
theorem
theorem
L7:
|.sin .| is PI -periodic
L8:
|.cos .| is PI -periodic
theorem
theorem
L9:
|.sin .| + |.cos .| is PI / 2 -periodic
theorem
L10:
sin ^2 is PI -periodic
L11:
cos ^2 is PI -periodic
theorem
theorem
L12:
sin (#) cos is PI -periodic
theorem
theorem
canceled;
L14:
for b, a being real number holds b + (a (#) sin ) is 2 * PI -periodic
L16:
for b, a being real number holds b + (a (#) cos ) is 2 * PI -periodic
theorem WW:
theorem
theorem NN:
theorem
theorem TT: