:: deftheorem defines -periodic FUNCT_9:def 1 :
for t being Real
for F being Function holds
( F is t -periodic iff ( t <> 0 & ( for x being Real 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) ) ) ) ) );