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

proof

per cases ( a <> 0 or a = 0 ) ;

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;

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

proof

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;

hence F is 1 -periodic by FUNCT_9:1; :: thesis: verum

end;

end;

end;

hence F is periodic by FUNCT_9:def 2; :: thesis: verum