consider
t
being
Real
such that
A1
:
F
is
t
periodic
by
Def2
;

F
is
t
periodic
by
A1
,
Th6
;
hence

F
is
periodic
;
:: thesis:
verum