let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, c, d being Real
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 x in A \ ['(a - c),(a + c)'] holds
f . x = 0
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 x in A \ ['(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 x in A \ ['(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 x in A \ ['(a - c),(a + c)'] holds
f . x = 0
let x be Real; :: thesis: ( x in A \ ['(a - c),(a + c)'] implies f . x = 0 )
assume A4: x in A \ ['(a - c),(a + c)'] ; :: thesis: f . x = 0
not x in ['(a - c),(a + c)'] by XBOOLE_0:def 5, A4;
hence f . x = 0 by FU710, A1, A2, A3; :: thesis: verum