theorem :: FUNCT_9:19

for t1, t2 being Real
for F being real-valued Function st t1 - t2 <> 0 & ( for x being Real st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ) holds
( F is t1 - t2 -periodic & F is periodic )