let t1, t2 be Real; :: thesis: for F being real-valued Function st t1 + t2 <> 0 & ( for x being Real st x in dom F holds

( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) holds

( F is t1 + t2 -periodic & F is periodic )

let F be real-valued Function; :: thesis: ( t1 + t2 <> 0 & ( for x being Real st x in dom F holds

( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) implies ( F is t1 + t2 -periodic & F is periodic ) )

assume that

A1: t1 + t2 <> 0 and

A2: for x being Real st x in dom F holds

( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ; :: thesis: ( F is t1 + t2 -periodic & F is periodic )

for x being Real st x in dom F holds

( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) )

hence ( F is t1 + t2 -periodic & F is periodic ) ; :: thesis: verum

( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) holds

( F is t1 + t2 -periodic & F is periodic )

let F be real-valued Function; :: thesis: ( t1 + t2 <> 0 & ( for x being Real st x in dom F holds

( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) implies ( F is t1 + t2 -periodic & F is periodic ) )

assume that

A1: t1 + t2 <> 0 and

A2: for x being Real st x in dom F holds

( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ; :: thesis: ( F is t1 + t2 -periodic & F is periodic )

for x being Real st x in dom F holds

( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) )

proof

then
F is t1 + t2 -periodic
by Th1, A1;
let x be Real; :: thesis: ( x in dom F implies ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) )

assume x in dom F ; :: thesis: ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) )

then A3: ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F ) by A2;

then A4: ( (x + t1) + t2 in dom F & (x - t1) - t2 in dom F ) by A2;

F . (x + (t1 + t2)) = F . ((x + t2) + t1)

.= F . ((x + t2) - t2) by A2, A3

.= F . x ;

hence ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) by A4; :: thesis: verum

end;assume x in dom F ; :: thesis: ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) )

then A3: ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F ) by A2;

then A4: ( (x + t1) + t2 in dom F & (x - t1) - t2 in dom F ) by A2;

F . (x + (t1 + t2)) = F . ((x + t2) + t1)

.= F . ((x + t2) - t2) by A2, A3

.= F . x ;

hence ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) by A4; :: thesis: verum

hence ( F is t1 + t2 -periodic & F is periodic ) ; :: thesis: verum