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 - t) ) ) 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 - t) ) ) 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 - t) ) ; :: 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 x in dom F ; :: thesis: ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) )
then A3: ( x + t in dom F & x - t in dom F ) by A2;
then A4: ( (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) - t) 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 A4; :: thesis: verum

end;

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