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)) )

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 x in dom F ; :: thesis: ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) )
then ( x + t in dom F & x - t in dom F ) by A1, Th1;
hence ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) ) by A1, Th13; :: thesis: verum

end;

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