let a, b, c be Real; :: thesis: ( a < b & b < c implies (TriangularFS (a,b,c)) | [.a,c.] = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) )
assume A1: ( a < b & b < c ) ; :: thesis: (TriangularFS (a,b,c)) | [.a,c.] = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])
set fac = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]);
A6: dom (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) = (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) \/ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by FUNCT_4:def 1
.= [.a,b.] \/ (dom ((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 ((TriangularFS (a,b,c)) | [.a,c.]) by FUNCT_2:def 1 ;
for x being object st x in dom ((TriangularFS (a,b,c)) | [.a,c.]) holds
((TriangularFS (a,b,c)) | [.a,c.]) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x

proof

let x be object ; :: thesis: ( x in dom ((TriangularFS (a,b,c)) | [.a,c.]) implies ((TriangularFS (a,b,c)) | [.a,c.]) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x )
assume A7: x in dom ((TriangularFS (a,b,c)) | [.a,c.]) ; :: thesis: ((TriangularFS (a,b,c)) | [.a,c.]) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x
then reconsider x = x as Real ;
((TriangularFS (a,b,c)) | [.a,c.]) . x = (TriangularFS (a,b,c)) . x by FUNCT_1:49, A7
.= ((((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x by A1, FUZNUM_1:def 7
.= (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]))) . x by FUNCT_4:14 ;
hence ((TriangularFS (a,b,c)) | [.a,c.]) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x by FUNCT_4:13, A6, A7; :: thesis: verum

end;

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