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

hence ( F is 2 * t -periodic & F is periodic ) ; :: thesis: verum

( 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

then
F is 2 * t -periodic
by A1, Th1;
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;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

hence ( F is 2 * t -periodic & F is periodic ) ; :: thesis: verum