let a, b, c, r be Real; :: thesis: for f being Function of REAL,REAL st a < b & b < c holds
(r (#) (TriangularFS (a,b,c))) | [.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 implies (r (#) (TriangularFS (a,b,c))) | [.a,c.] = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.]) )
set fab = AffineMap ((1 / (b - a)),(- (a / (b - a))));
set fbc = AffineMap ((- (1 / (c - b))),(c / (c - b)));
assume A2: ( a < b & b < c ) ; :: thesis: (r (#) (TriangularFS (a,b,c))) | [.a,c.] = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.])
hence (r (#) (TriangularFS (a,b,c))) | [.a,c.] = (r (#) (TriangularFS (a,b,c))) | ['a,c'] by XXREAL_0:2, INTEGRA5:def 3
.= r (#) ((TriangularFS (a,b,c)) | ['a,c']) by FUZZY_7:10
.= r (#) ((TriangularFS (a,b,c)) | [.a,c.]) by A2, XXREAL_0:2, INTEGRA5:def 3
.= r (#) (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by Th4, A2
.= (r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* (r (#) ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by Th500
.= (r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ['a,b'])) +* (r (#) ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by A2, INTEGRA5:def 3
.= (r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ['a,b'])) +* (r (#) ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | ['b,c'])) by A2, INTEGRA5:def 3
.= ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | ['a,b']) +* (r (#) ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | ['b,c'])) by FUZZY_7:10
.= ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | ['a,b']) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | ['b,c']) by FUZZY_7:10
.= ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | ['a,b']) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.]) by A2, INTEGRA5:def 3
.= ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.]) by A2, INTEGRA5:def 3 ;
:: thesis: verum