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

proof

let x be Real; :: thesis: ( x in dom F implies ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) )
assume A3: x in dom F ; :: thesis: ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) )
then A4: ( x + t in dom F & x - t in dom F ) by A2;
then A5: ( (x + t) + t in dom F & (x - t) - t in dom F ) by A2;
F . (x + (2 * t)) = F . ((x + t) + t)
.= (F . (x + t)) " by A2, A4
.= ((F . x) ") " by A2, A3
.= F . x ;
hence ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) by A5; :: thesis: verum

end;

then F is 2 * t -periodic by A1, Th1;
hence ( F is 2 * t -periodic & F is periodic ) ; :: thesis: verum