consider t being Real such that
A2: F is t -periodic by Def2;
F " is t -periodic by A2, Th11;
hence F " is periodic ; :: thesis: verum