let t be Real; :: thesis: for F being real-valued Function st F is t -periodic holds
F " is t -periodic
let F be real-valued Function; :: thesis: ( F is t -periodic implies F " is t -periodic )
assume A1: F is t -periodic ; :: thesis: F " is t -periodic
then A2: ( t <> 0 & ( for x being Real st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1;
for x being Real st x in dom (F ") holds
( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) )

proof

let x be Real; :: thesis: ( x in dom (F ") implies ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) ) )
assume A3: x in dom (F ") ; :: thesis: ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) )
then A4: x in dom F by VALUED_1:def 7;
then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1;
then A6: ( x + t in dom (F ") & x - t in dom (F ") ) by VALUED_1:def 7;
(F ") . x = (F . x) " by A3, VALUED_1:def 7
.= (F . (x + t)) " by A1, A4
.= (F ") . (x + t) by A6, VALUED_1:def 7 ;
hence ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) ) by A5, VALUED_1:def 7; :: thesis: verum

end;

hence F " is t -periodic by A2, Th1; :: thesis: verum