let t1, t2 be Real; :: thesis: for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 holds

F is t1 - t2 -periodic

let F be real-valued Function; :: thesis: ( F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 implies F is t1 - t2 -periodic )

assume A1: ( F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 ) ; :: thesis: F is t1 - t2 -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)) )

F is t1 - t2 -periodic

let F be real-valued Function; :: thesis: ( F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 implies F is t1 - t2 -periodic )

assume A1: ( F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 ) ; :: thesis: F is t1 - t2 -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

hence
F is t1 - t2 -periodic
by A1, Th1; :: thesis: verum
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 A2: x in dom F ; :: thesis: ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) )

then ( x + t1 in dom F & x - t1 in dom F ) by A1, Th1;

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

A4: x - t2 in dom F by A1, Th1, A2;

then F . ((x - t2) + t1) = F . (x - t2) by A1

.= F . ((x - t2) + t2) by A1, A4

.= F . x ;

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

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

then ( x + t1 in dom F & x - t1 in dom F ) by A1, Th1;

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

A4: x - t2 in dom F by A1, Th1, A2;

then F . ((x - t2) + t1) = F . (x - t2) by A1

.= F . ((x - t2) + t2) by A1, A4

.= F . x ;

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