let a, b, c, r be Real; :: thesis: for f being Function of REAL,REAL st a < b & b < c & ( for x being Real holds f . x = (r (#) (TriangularFS (a,b,c))) . x ) holds
f | [.a,c.] = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])
let f be Function of REAL,REAL; :: thesis: ( a < b & b < c & ( for x being Real holds f . x = (r (#) (TriangularFS (a,b,c))) . x ) implies f | [.a,c.] = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.]) )
assume that
A1: ( a < b & b < c ) and
A3: for x being Real holds f . x = (r (#) (TriangularFS (a,b,c))) . x ; :: thesis: f | [.a,c.] = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])
set fac = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.]);
A6: dom (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])) = (dom ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.])) \/ (dom ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])) by FUNCT_4:def 1
.= [.a,b.] \/ (dom ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] by FUNCT_2:def 1
.= [.a,c.] by XXREAL_1:165, A1
.= dom (f | [.a,c.]) by FUNCT_2:def 1 ;
for x being object st x in dom (f | [.a,c.]) holds
(f | [.a,c.]) . x = (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])) . x

proof

let x be object ; :: thesis: ( x in dom (f | [.a,c.]) implies (f | [.a,c.]) . x = (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])) . x )
assume A7: x in dom (f | [.a,c.]) ; :: thesis: (f | [.a,c.]) . x = (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])) . x
then reconsider x = x as Real ;
set F = AffineMap ((1 / (b - a)),(- (a / (b - a))));
(f | [.a,c.]) . x = f . x by A7, FUNCT_1:49
.= (r (#) (TriangularFS (a,b,c))) . x by A3
.= r * ((TriangularFS (a,b,c)) . x) by VALUED_1:6
.= r * (((TriangularFS (a,b,c)) | [.a,c.]) . x) by A7, FUNCT_1:49
.= r * ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x) by A1, Th4
.= (r (#) (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]))) . x by VALUED_1:6
.= ((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* (r (#) ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]))) . x by Th500
.= (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* (r (#) ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]))) . x by MESFUN6C:41
.= (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])) . x by MESFUN6C:41 ;
hence (f | [.a,c.]) . x = (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])) . x ; :: thesis: verum

end;

hence f | [.a,c.] = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.]) by FUNCT_1:2, A6; :: thesis: verum