let t be Real; :: thesis: for F being real-valued Function holds

( F is t -periodic iff ( t <> 0 & ( for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )

let F be real-valued Function; :: thesis: ( F is t -periodic iff ( t <> 0 & ( for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )

thus ( F is t -periodic implies ( t <> 0 & ( for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ) :: 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 = F . (x + t) ) ) implies F is t -periodic )

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

for x being Real holds

( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) )

( F is t -periodic iff ( t <> 0 & ( for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )

let F be real-valued Function; :: thesis: ( F is t -periodic iff ( t <> 0 & ( for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )

thus ( F is t -periodic implies ( t <> 0 & ( for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ) :: 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 = F . (x + t) ) ) implies F is t -periodic )

proof

assume A2:
( t <> 0 & ( for x being Real st x in dom F holds
assume A1:
F is t -periodic
; :: 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 = F . (x + t) ) ) )

for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) )

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1; :: thesis: verum

end;( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) )

for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) )

proof

hence
( t <> 0 & ( for x being Real st x in dom F holds
let x be Real; :: thesis: ( x in dom F implies ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) )

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

then (x - t) + t in dom F ;

hence ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) by A1; :: thesis: verum

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

then (x - t) + t in dom F ;

hence ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) by A1; :: thesis: verum

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1; :: thesis: verum

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

for x being Real holds

( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) )

proof

hence
F is t -periodic
by A2; :: thesis: verum
let x be Real; :: thesis: ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) )

( x in dom F iff x + t in dom F )

end;( x in dom F iff x + t in dom F )

proof

hence
( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) )
by A2; :: thesis: verum
( x + t in dom F implies x in dom F )

end;proof

hence
( x in dom F iff x + t in dom F )
by A2; :: thesis: verum
assume
x + t in dom F
; :: thesis: x in dom F

then (x + t) - t in dom F by A2;

hence x in dom F ; :: thesis: verum

end;then (x + t) - t in dom F by A2;

hence x in dom F ; :: thesis: verum