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
f = b (#) (TriangularFS ((a - c),a,(a + c)))
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 f = b (#) (TriangularFS ((a - c),a,(a + c))) )
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ; :: thesis: f = b (#) (TriangularFS ((a - c),a,(a + c)))
set g = b (#) (TriangularFS ((a - c),a,(a + c)));
A4: dom f = REAL by FUNCT_2:def 1
.= dom (b (#) (TriangularFS ((a - c),a,(a + c)))) by FUNCT_2:def 1 ;
for x being object st x in dom f holds
f . x = (b (#) (TriangularFS ((a - c),a,(a + c)))) . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = (b (#) (TriangularFS ((a - c),a,(a + c)))) . x )
assume x in dom f ; :: thesis: f . x = (b (#) (TriangularFS ((a - c),a,(a + c)))) . x
then reconsider x = x as Real ;
(b (#) (TriangularFS ((a - c),a,(a + c)))) . x = b * ((TriangularFS ((a - c),a,(a + c))) . x) by VALUED_1:6
.= b * (max (0,(1 - |.((x - a) / c).|))) by FUZZY_5:65, A2
.= max ((b * 0),(b * (1 - |.((x - a) / c).|))) by FUZZY_2:41, A1
.= max (0,(b - (b * |.((x - a) / c).|)))
.= max (0,(b - (|.b.| * |.((x - a) / c).|))) by A1, ABSVALUE:def 1
.= max (0,(b - |.(b * ((x - a) / c)).|)) by COMPLEX1:65
.= max (0,(b - |.((b * (x - a)) / c).|)) by XCMPLX_1:74
.= f . x by A3 ;
hence f . x = (b (#) (TriangularFS ((a - c),a,(a + c)))) . x ; :: thesis: verum

end;

hence f = b (#) (TriangularFS ((a - c),a,(a + c))) by A4, FUNCT_1:def 11; :: thesis: verum