:: deftheorem Def2 defines periodic FUNCT_9:def 2 :
for F being Function holds
( F is periodic iff ex t being Real st F is t -periodic );