theorem :: FUNCT_9:37
for t, a being Real st t <> 0 holds
REAL --> a is t -periodic by Lm1;