let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st a < b & b < c & f = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[) holds
max+ f = TriangularFS (a,b,c)
let f be Function of REAL,REAL; :: thesis: ( a < b & b < c & f = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[) implies max+ f = TriangularFS (a,b,c) )
assume that
A1: ( a < b & b < c ) and
A2: f = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[) ; :: thesis: max+ f = TriangularFS (a,b,c)
A3: dom (max+ f) = dom f by RFUNCT_3:def 10
.= REAL by FUNCT_2:def 1 ;
A31: REAL = dom (TriangularFS (a,b,c)) by FUNCT_2:def 1;
for x being object st x in dom (TriangularFS (a,b,c)) holds
(TriangularFS (a,b,c)) . x = (max+ f) . x

proof

let x be object ; :: thesis: ( x in dom (TriangularFS (a,b,c)) implies (TriangularFS (a,b,c)) . x = (max+ f) . x )
assume B1: x in dom (TriangularFS (a,b,c)) ; :: thesis: (TriangularFS (a,b,c)) . x = (max+ f) . x
then reconsider x = x as Real ;
A6: (max+ f) . x = max+ (f . x) by RFUNCT_3:def 10, A3, B1
.= max ((f . x),0) by RFUNCT_3:def 1 ;

per cases ( x in [.a,c.] or not x in [.a,c.] ) ;

suppose D1: x in [.a,c.] ; :: thesis: (TriangularFS (a,b,c)) . x = (max+ f) . x

then D2: f . x = ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[)) | [.a,c.]) . x by FUNCT_1:49, A2
.= (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x by FUZZY_7:20, A1
.= ((TriangularFS (a,b,c)) | [.a,c.]) . x by Th4, A1
.= (TriangularFS (a,b,c)) . x by FUNCT_1:49, D1 ;
f . x >= 0 by D2, A1, D1, Th18;
hence (TriangularFS (a,b,c)) . x = (max+ f) . x by D2, XXREAL_0:def 10, A6; :: thesis: verum

end;

suppose not x in [.a,c.] ; :: thesis: (TriangularFS (a,b,c)) . x = (max+ f) . x

then ( x < a or c < x ) ;
then C1: not x in ].a,c.[ by XXREAL_1:4;
then C2s: f . x <= 0 by A1, Th16, A2;
(TriangularFS (a,b,c)) . x = (AffineMap (0,0)) . x by FUZZY_8:48, C1, A1
.= (0 * x) + 0 by FCONT_1:def 4 ;
hence (TriangularFS (a,b,c)) . x = (max+ f) . x by C2s, A6, XXREAL_0:def 10; :: thesis: verum

end;

end;

end;

hence max+ f = TriangularFS (a,b,c) by FUNCT_1:2, A3, A31; :: thesis: verum