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

proof

let x be object ; :: thesis: ( x in dom (r (#) (TriangularFS (a,b,c))) implies (r (#) (TriangularFS (a,b,c))) . x = (max+ f) . x )
assume B1: x in dom (r (#) (TriangularFS (a,b,c))) ; :: thesis: (r (#) (TriangularFS (a,b,c))) . x = (max+ f) . x
then reconsider x = x as Real ;
dom F = REAL by FUNCT_2:def 1;
then A7s: dom (max+ F) = REAL by RFUNCT_3:def 10;
A6: (max+ f) . x = max+ (f . x) by RFUNCT_3:def 10, A3, B1
.= max (((r (#) F) . x),0) by A2, RFUNCT_3:def 1
.= max ((r * (F . x)),0) by VALUED_1:6
.= (((r * (F . x)) + 0) + |.((r * (F . x)) - 0).|) / 2 by COMPLEX1:74
.= ((r * (F . x)) + (|.r.| * |.(F . x).|)) / 2 by COMPLEX1:65
.= ((r * (F . x)) + (r * |.(F . x).|)) / 2 by COMPLEX1:43, R1 ;
(r (#) (TriangularFS (a,b,c))) . x = r * ((TriangularFS (a,b,c)) . x) by VALUED_1:6
.= r * ((max+ F) . x) by A1, Th19
.= r * (max+ (F . x)) by RFUNCT_3:def 10, A7s, B1
.= r * (max ((F . x),0)) by RFUNCT_3:def 1
.= r * ((((F . x) + 0) + |.((F . x) - 0).|) / 2) by COMPLEX1:74
.= r * (((F . x) + |.(F . x).|) / 2) ;
hence (r (#) (TriangularFS (a,b,c))) . x = (max+ f) . x by A6; :: thesis: verum

end;

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