{ 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

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

proof

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

proof

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;

hence f = TriangularFS ((a - b),a,(a + b)) by FUNCT_1:2, A6; :: thesis: verum

end;

hence f in { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) } by A4; :: thesis: verum

end;

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