let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0
let f be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) implies for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0 )
assume A1: ( b > 0 & c > 0 ) ; :: thesis: ( ex x being Real st not f . x = max (0,(b - |.((b * (x - a)) / c).|)) or for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0 )
then B1: - c < 0 ;
assume A2: for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ; :: thesis: for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0
for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0

proof

let x be Real; :: thesis: ( not x in ['(a - c),(a + c)'] implies f . x = 0 )
assume A4: not x in ['(a - c),(a + c)'] ; :: thesis: f . x = 0
( a < a + c & a - c < a ) by XREAL_1:44, XREAL_1:29, A1;
then A3: not x in [.(a - c),(a + c).] by INTEGRA5:def 3, A4, XXREAL_0:2;

per cases ( x < a - c or a + c < x ) by A3;

suppose x < a - c ; :: thesis: f . x = 0

then B2: x - a < (a - c) - a by XREAL_1:9;
then b * (x - a) < b * (- c) by A1, XREAL_1:68;
then (b * (x - a)) / c < (- (c * b)) / c by A1, XREAL_1:74;
then (b * (x - a)) / c < - ((c * b) / c) by XCMPLX_1:187;
then (b * (x - a)) / c < - b by A1, XCMPLX_1:89;
then B4: ((b * (x - a)) / c) + b < (- b) + b by XREAL_1:6;
thus f . x = max (0,(b - |.((b * (x - a)) / c).|)) by A2
.= max (0,(b - (- ((b * (x - a)) / c)))) by COMPLEX1:70, A1, B1, B2
.= 0 by B4, XXREAL_0:def 10 ; :: thesis: verum

end;

suppose a + c < x ; :: thesis: f . x = 0

then C2: x - a > (a + c) - a by XREAL_1:9;
then b * (x - a) > b * c by A1, XREAL_1:68;
then (b * (x - a)) / c > (b * c) / c by A1, XREAL_1:74;
then (b * (x - a)) / c > b by A1, XCMPLX_1:89;
then C4: ((b * (x - a)) / c) - ((b * (x - a)) / c) > b - ((b * (x - a)) / c) by XREAL_1:9;
thus f . x = max (0,(b - |.((b * (x - a)) / c).|)) by A2
.= max (0,(b - ((b * (x - a)) / c))) by COMPLEX1:43, A1, C2
.= 0 by C4, XXREAL_0:def 10 ; :: thesis: verum

end;

end;

end;

hence for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0 ; :: thesis: verum