let f be Function of REAL,REAL; :: thesis: for a, b being Real st b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) holds

f is continuous

let a, b be Real; :: thesis: ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is continuous )

assume A2: b > 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(1 - |.((x - a) / b).|)) or f is continuous )

then A4: ( a - b < a & a < a + b ) by XREAL_1:44, XREAL_1:29;

assume A1: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis: f is continuous

f = TriangularFS ((a - b),a,(a + b))

f is continuous

let a, b be Real; :: thesis: ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is continuous )

assume A2: b > 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(1 - |.((x - a) / b).|)) or f is continuous )

then A4: ( a - b < a & a < a + b ) by XREAL_1:44, XREAL_1:29;

assume A1: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis: f is continuous

f = TriangularFS ((a - b),a,(a + b))

proof

hence
f is continuous
by A4, FUZNUM_1:30; :: thesis: verum
A6:
( dom f = REAL & REAL = dom (TriangularFS ((a - b),a,(a + b))) )
by FUNCT_2:def 1;

for x being object st x in dom f holds

f . x = (TriangularFS ((a - b),a,(a + b))) . x

end;for x being object st x in dom f holds

f . x = (TriangularFS ((a - b),a,(a + b))) . x

proof

hence
f = TriangularFS ((a - b),a,(a + b))
by FUNCT_1:2, A6; :: thesis: verum
let x be object ; :: thesis: ( x in dom f implies f . x = (TriangularFS ((a - b),a,(a + b))) . x )

assume x in dom f ; :: thesis: f . x = (TriangularFS ((a - b),a,(a + b))) . x

then x in REAL by FUNCT_2:def 1;

then reconsider x = x as Real ;

f . x = max (0,(1 - |.((x - a) / b).|)) by A1;

hence f . x = (TriangularFS ((a - b),a,(a + b))) . x by TR6, A2; :: thesis: verum

end;assume x in dom f ; :: thesis: f . x = (TriangularFS ((a - b),a,(a + b))) . x

then x in REAL by FUNCT_2:def 1;

then reconsider x = x as Real ;

f . x = max (0,(1 - |.((x - a) / b).|)) by A1;

hence f . x = (TriangularFS ((a - b),a,(a + b))) . x by TR6, A2; :: thesis: verum