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
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 & d > 0 & ( for x being Real holds f . x = min (d,(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 that
A1: ( b > 0 & c > 0 ) and
A2: d > 0 and
A3: for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0
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
f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by A3
.= 0 by FU710b, A1, A2, A4 ;
hence f . x = 0 ; :: thesis: verum