begin
:: deftheorem Def1 defines -periodic FUNCT_9:def 1 :
for t being real number
for F being Function holds
( F is t -periodic iff ( t <> 0 & ( for x being real number holds
( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ) ) );
:: deftheorem Def2 defines periodic FUNCT_9:def 2 :
for F being Function holds
( F is periodic iff ex t being real number st F is t -periodic );
theorem Th1:
theorem
theorem
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm1:
sin is 2 * PI -periodic
begin
Lm2:
cos is 2 * PI -periodic
theorem
theorem
Lm3:
cosec is 2 * PI -periodic
Lm4:
sec is 2 * PI -periodic
theorem
theorem
Lm5:
tan is PI -periodic
Lm6:
cot is PI -periodic
theorem
theorem
Lm7:
|.sin.| is PI -periodic
Lm8:
|.cos.| is PI -periodic
theorem
theorem
Lm9:
|.sin.| + |.cos.| is PI / 2 -periodic
theorem
Lm10:
sin ^2 is PI -periodic
Lm11:
cos ^2 is PI -periodic
theorem
theorem
Lm12:
sin (#) cos is PI -periodic
theorem
theorem
canceled;
Lm13:
for b, a being real number holds b + (a (#) sin) is 2 * PI -periodic
Lm14:
for b, a being real number holds b + (a (#) cos) is 2 * PI -periodic
theorem Th34:
theorem
theorem Th36:
theorem
theorem Th38: