let F be Function of REAL,REAL; :: thesis: for a, b, c, d being Real st ( for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) holds

F is periodic

let a, b, c, d be Real; :: thesis: ( ( for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) implies F is periodic )

assume A0: for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ; :: thesis: F is periodic

ex t being Real st F is t -periodic

F is periodic

let a, b, c, d be Real; :: thesis: ( ( for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) implies F is periodic )

assume A0: for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ; :: thesis: F is periodic

ex t being Real st F is t -periodic

proof
end;

hence
F is periodic
by FUNCT_9:def 2; :: thesis: verumper cases
( a <> 0 or a = 0 )
;

end;

suppose A1:
a <> 0
; :: thesis: ex t being Real st F is t -periodic

take
((2 * PI) / a) * 1
; :: thesis: F is ((2 * PI) / a) * 1 -periodic

thus F is ((2 * PI) / a) * 1 -periodic by TrF160, A0, A1; :: thesis: verum

end;thus F is ((2 * PI) / a) * 1 -periodic by TrF160, A0, A1; :: thesis: verum

suppose A5:
a = 0
; :: thesis: ex t being Real st F is t -periodic

take
1
; :: thesis: F is 1 -periodic

for x being Real st x in dom F holds

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

end;for x being Real st x in dom F holds

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

proof

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

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

A4A: ( x + 1 in REAL & x - 1 in REAL ) by XREAL_0:def 1;

F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) by A0

.= max (0,(min (1,((c * (sin ((0 * (x + 1)) + b))) + d)))) by A5 ;

hence ( x + 1 in dom F & x - 1 in dom F & F . x = F . (x + 1) ) by A4A, FUNCT_2:def 1, A0, A5; :: thesis: verum

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

A4A: ( x + 1 in REAL & x - 1 in REAL ) by XREAL_0:def 1;

F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) by A0

.= max (0,(min (1,((c * (sin ((0 * (x + 1)) + b))) + d)))) by A5 ;

hence ( x + 1 in dom F & x - 1 in dom F & F . x = F . (x + 1) ) by A4A, FUNCT_2:def 1, A0, A5; :: thesis: verum