theorem :: FUNCT_9:12

for t being Real
for F being real-valued Function st F is t -periodic holds
F ^2 is t -periodic by Th4;