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

end;

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