let a, b, c, d be Real; :: thesis: for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 )
let f be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & d > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies ( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 ) )
assume A1: ( b > 0 & c > 0 & d > 0 ) ; :: thesis: ( ex x being Real st not f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) or ( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 ) )
assume A3: for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: ( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 )
( a < a + c & a - c < a ) by XREAL_1:44, XREAL_1:29, A1;
then A4: a - c < a + c by XXREAL_0:2;
A2: f . (lower_bound ['(a - c),(a + c)']) = f . (a - c) by FUZZY_6:7, A4
.= min (d,(max (0,(b - |.((b * ((a - c) - a)) / c).|)))) by A3
.= min (d,(max (0,(b - |.(((- 1) * (c * b)) / c).|))))
.= min (d,(max (0,(b - |.((- 1) * ((c * b) / c)).|)))) by XCMPLX_1:74
.= min (d,(max (0,(b - |.(- ((c * b) / c)).|))))
.= min (d,(max (0,(b - |.(- b).|)))) by A1, XCMPLX_1:89
.= min (d,(max (0,(b - (- (- b)))))) by ABSVALUE:def 1, A1
.= 0 by XXREAL_0:def 9, A1 ;
f . (upper_bound ['(a - c),(a + c)']) = f . (a + c) by FUZZY_6:7, A4
.= min (d,(max (0,(b - |.((b * ((a + c) - a)) / c).|)))) by A3
.= min (d,(max (0,(b - |.b.|)))) by A1, XCMPLX_1:89
.= min (d,(max (0,(b - b)))) by ABSVALUE:def 1, A1
.= min (d,0) ;
hence ( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 ) by A2, XXREAL_0:def 9, A1; :: thesis: verum