let f be Function of REAL,REAL; :: thesis: for a, b, c, d, e being Real st ( for x being Real holds f . x = min (d,(max (e,(b - |.((b * (x - a)) / c).|)))) ) holds
for y being Real holds f . (a - y) = f . (a + y)
let a, b, c, d, e be Real; :: thesis: ( ( for x being Real holds f . x = min (d,(max (e,(b - |.((b * (x - a)) / c).|)))) ) implies for y being Real holds f . (a - y) = f . (a + y) )
assume A2: for x being Real holds f . x = min (d,(max (e,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: for y being Real holds f . (a - y) = f . (a + y)
let y be Real; :: thesis: f . (a - y) = f . (a + y)
thus f . (a - y) = min (d,(max (e,(b - |.((b * ((a - y) - a)) / c).|)))) by A2
.= min (d,(max (e,(b - |.((- (y * b)) * (1 / c)).|)))) by XCMPLX_1:99
.= min (d,(max (e,(b - |.(- ((y * b) * (1 / c))).|))))
.= min (d,(max (e,(b - |.(- ((y * b) / c)).|)))) by XCMPLX_1:99
.= min (d,(max (e,(b - |.((b * ((a + y) - a)) / c).|)))) by COMPLEX1:52
.= f . (a + y) by A2 ; :: thesis: verum