{ f where f is Function of REAL,REAL, a, b is Real : ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) ) } c= { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) }

proof

hence
{ f where f is Function of REAL,REAL, a, b is Real : ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) ) } c= Membership_Funcs REAL
by TR2XX; :: thesis: verum
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { f where f is Function of REAL,REAL, a, b is Real : ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) ) } or f in { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) } )

assume f in { f where f is Function of REAL,REAL, a, b is Real : ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) ) } ; :: thesis: f in { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) }

then consider f0 being Function of REAL,REAL, a, b being Real such that

A1: f = f0 and

A2: b > 0 and

A3: for x being Real holds f0 . x = max (0,(1 - |.((x - a) / b).|)) ;

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

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

end;assume f in { f where f is Function of REAL,REAL, a, b is Real : ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) ) } ; :: thesis: f in { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) }

then consider f0 being Function of REAL,REAL, a, b being Real such that

A1: f = f0 and

A2: b > 0 and

A3: for x being Real holds f0 . x = max (0,(1 - |.((x - a) / b).|)) ;

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

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

proof

hence
f in { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) }
by A4; :: thesis: verum
reconsider f = f as Function of REAL,REAL by A1;

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;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

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, A3;

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, A3;

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