let a, b, c be Real; :: thesis: ( a < b & b < c implies for x being Real holds (TriangularFS (a,b,c)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.[) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[)) . x)))) )
assume A1: ( a < b & b < c ) ; :: thesis: for x being Real holds (TriangularFS (a,b,c)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.[) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[)) . x))))
set f = TriangularFS (a,b,c);
for x being Real holds (TriangularFS (a,b,c)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.[) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[)) . x))))

proof

let x be Real; :: thesis: (TriangularFS (a,b,c)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.[) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[)) . x))))
set a1 = 1 / (b - a);
set b1 = - (a / (b - a));
set p1 = 1 / (c - b);
set q1 = c / (c - b);
b1: ( b - a > a - a & b - b < c - b ) by XREAL_1:9, A1;
a * 1 < 1 * c by A1, XXREAL_0:2;
then (- (- a)) * ((1 / (b - a)) / (1 / (b - a))) < c * 1 by XCMPLX_1:60, b1;
then (- (- a)) * ((1 / (b - a)) / (1 / (b - a))) < c * ((1 / (c - b)) / (1 / (c - b))) by XCMPLX_1:60, b1;
then ((- (- a)) * (1 / (b - a))) / (1 / (b - a)) < c * ((1 / (c - b)) / (1 / (c - b))) by XCMPLX_1:74;
then ((- (- a)) * (1 / (b - a))) / (1 / (b - a)) < (c * (1 / (c - b))) / (1 / (c - b)) by XCMPLX_1:74;
then (- ((- a) * (1 / (b - a)))) / (1 / (b - a)) < ((c * 1) / (c - b)) / (1 / (c - b)) by XCMPLX_1:74;
then (- (((- a) * 1) / (b - a))) / (1 / (b - a)) < (c / (c - b)) / (1 / (c - b)) by XCMPLX_1:74;
then B3: (- (- (a / (b - a)))) / (1 / (b - a)) < (c / (c - b)) / (1 / (c - b)) by XCMPLX_1:187;
B2: (1 - (- (a / (b - a)))) / (1 / (b - a)) = (1 + (a / (b - a))) * (b - a) by XCMPLX_1:100
.= (b - a) + ((a / (b - a)) * (b - a))
.= (b - a) + a by XCMPLX_1:87, b1
.= b ;
Bb: (1 - (c / (c - b))) / (- (1 / (c - b))) = - ((1 - (c / (c - b))) / (1 / (c - b))) by XCMPLX_1:188
.= - ((1 - (c / (c - b))) * (c - b)) by XCMPLX_1:100
.= - ((c - b) - ((c / (c - b)) * (c - b)))
.= - ((c - b) - c) by XCMPLX_1:87, b1
.= b ;
B5: (- (- (a / (b - a)))) / (1 / (b - a)) = (b - a) * ((a / (b - a)) / 1) by XCMPLX_1:81
.= a by XCMPLX_1:87, b1 ;
B7: (c / (c - b)) / (1 / (c - b)) = (c - b) * ((c / (c - b)) / 1) by XCMPLX_1:81
.= c by XCMPLX_1:87, b1 ;
a < c by A1, XXREAL_0:2;
then B9: c - a > a - a by XREAL_1:9;
((c / (c - b)) - (- (a / (b - a)))) / ((1 / (b - a)) + (1 / (c - b))) = ((c / (c - b)) + (a / (b - a))) / ((1 / (b - a)) + (1 / (c - b)))
.= (((c * (b - a)) + (a * (c - b))) / ((b - a) * (c - b))) / ((1 / (b - a)) + (1 / (c - b))) by XCMPLX_1:116, b1
.= (((((c * b) - (c * a)) + (a * c)) - (a * b)) / ((b - a) * (c - b))) / (((1 * (b - a)) + (1 * (c - b))) / ((b - a) * (c - b))) by XCMPLX_1:116, b1
.= ((c - a) * b) / (c - a) by XCMPLX_1:55, b1
.= b by XCMPLX_1:89, B9 ;
hence (TriangularFS (a,b,c)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.[) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[)) . x)))) by B5, B7, Bb, b1, B3, asymTT6, B2; :: thesis: verum

end;

hence for x being Real holds (TriangularFS (a,b,c)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.[) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[)) . x)))) ; :: thesis: verum