theorem :: FUNCT_9:16

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