theorem :: FUNCT_9:15
for t1, t2 being Real
for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 holds
F is t1 + t2 -periodic