let a, b, c be Real; :: thesis: ( b > 0 & c > 0 implies for x being Real st not x in ['(a - c),(a + c)'] holds
max (0,(b - |.((b * (x - a)) / c).|)) = 0 )
assume that
A1: b > 0 and
A2: c > 0 ; :: thesis: for x being Real st not x in ['(a - c),(a + c)'] holds
max (0,(b - |.((b * (x - a)) / c).|)) = 0
let x be Real; :: thesis: ( not x in ['(a - c),(a + c)'] implies max (0,(b - |.((b * (x - a)) / c).|)) = 0 )
assume A4: not x in ['(a - c),(a + c)'] ; :: thesis: max (0,(b - |.((b * (x - a)) / c).|)) = 0
deffunc H₁( Element of REAL ) -> Element of REAL = In ((max (0,(b - |.((b * ($1 - a)) / c).|))),REAL);
consider h being Function of REAL,REAL such that
A5: for x being Element of REAL holds h . x = H₁(x) from FUNCT_2:sch 4();
A6: for x being Real holds h . x = max (0,(b - |.((b * (x - a)) / c).|))

proof

let x be Real; :: thesis: h . x = max (0,(b - |.((b * (x - a)) / c).|))
reconsider x = x as Element of REAL by XREAL_0:def 1;
h . x = In ((max (0,(b - |.((b * (x - a)) / c).|))),REAL) by A5;
hence h . x = max (0,(b - |.((b * (x - a)) / c).|)) ; :: thesis: verum

end;

hence 0 = h . x by A4, FUZZY_7:19, A1, A2
.= max (0,(b - |.((b * (x - a)) / c).|)) by A6 ;
:: thesis: verum