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
integral (f,['a,c']) = (r * (c - a)) / 2
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 integral (f,['a,c']) = (r * (c - a)) / 2 )
assume that
A1: ( a < b & b < c ) and
A2: for x being Real holds f . x = (r (#) (TriangularFS (a,b,c))) . x ; :: thesis: integral (f,['a,c']) = (r * (c - a)) / 2
A5: f | [.a,c.] = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.]) by Th7, A1, A2;
set fa = r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))));
set fc = r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))));
A7: ( b - a <> 0 & c - b <> 0 ) by A1;
A4: (r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) . b = r * ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b) by VALUED_1:6
.= r * (((1 / (b - a)) * b) + (- (a / (b - a)))) by FCONT_1:def 4
.= r * (((1 / (b - a)) * b) - (a / (b - a)))
.= r * ((b / (b - a)) - (a / (b - a))) by XCMPLX_1:99
.= r * ((b - a) / (b - a)) by XCMPLX_1:120
.= r * 1 by XCMPLX_1:60, A7
.= r * ((c - b) / (c - b)) by XCMPLX_1:60, A7
.= r * ((c / (c - b)) - (b / (c - b))) by XCMPLX_1:120
.= r * ((c / (c - b)) - ((1 / (c - b)) * b)) by XCMPLX_1:99
.= r * (((- (1 / (c - b))) * b) + (c / (c - b)))
.= r * ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b) by FCONT_1:def 4
.= (r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) . b by VALUED_1:6 ;
set ba = b - a;
set a1 = 1 / (b - a);
set b1 = - (a / (b - a));
set c1 = c - b;
thus integral (f,['a,c']) = (integral ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))),['a,b'])) + (integral ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))),['b,c'])) by FUZZY_8:11, A1, A4, A5
.= (integral ((AffineMap ((r * (1 / (b - a))),(r * (- (a / (b - a)))))),['a,b'])) + (integral ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))),['b,c'])) by FUZZY_7:13
.= ((b - a) * ((((r * (1 / (b - a))) * (b + a)) / 2) + (r * (- (a / (b - a)))))) + (integral ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))),['b,c'])) by FUZZY_8:42, A1
.= ((b - a) * ((((r * (1 / (b - a))) * (b + a)) / 2) + (r * (- (a / (b - a)))))) + (integral ((AffineMap ((r * (- (1 / (c - b)))),(r * (c / (c - b))))),['b,c'])) by FUZZY_7:13
.= ((b - a) * ((((r * (1 / (b - a))) * (b + a)) / 2) + (r * (- (a / (b - a)))))) + ((c - b) * ((((r * (- (1 / (c - b)))) * (c + b)) / 2) + (r * (c / (c - b))))) by FUZZY_8:42, A1
.= ((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (r * (- (a / (b - a)))))) + ((c - b) * ((((r * (- (1 / (c - b)))) * (c + b)) / 2) + (r * (c / (c - b))))) by XCMPLX_1:99
.= ((b - a) * ((((r / (b - a)) * (b + a)) / 2) - (r * (a / (b - a))))) + ((c - b) * ((- (((r * (1 / (c - b))) * (c + b)) / 2)) + (r * (c / (c - b)))))
.= ((b - a) * ((((r / (b - a)) * (b + a)) / 2) - (r * (a / (b - a))))) + ((c - b) * ((- (((r / (c - b)) * (c + b)) / 2)) + (r * (c / (c - b))))) by XCMPLX_1:99
.= (((b - a) * (((r / (b - a)) * (b + a)) / 2)) - ((b - a) * (r * (a / (b - a))))) + (((c - b) * (- (((r / (c - b)) * (c + b)) / 2))) + ((c - b) * (r * (c / (c - b)))))
.= (((((b - a) * (r / (b - a))) * (b + a)) / 2) - ((b - a) * (r * (a / (b - a))))) + (((c - b) * (- (((r / (c - b)) * (c + b)) / 2))) + ((c - b) * ((r * c) / (c - b)))) by XCMPLX_1:74
.= ((((((b - a) * r) / (b - a)) * (b + a)) / 2) - ((b - a) * (r * (a / (b - a))))) + (((c - b) * (- (((r / (c - b)) * (c + b)) / 2))) + ((c - b) * ((r * c) / (c - b)))) by XCMPLX_1:74
.= ((((((b - a) * r) / (b - a)) * (b + a)) / 2) - ((b - a) * (r * (a / (b - a))))) + (((c - b) * (- (((r / (c - b)) * (c + b)) / 2))) + (((c - b) * (r * c)) / (c - b))) by XCMPLX_1:74
.= (((((((b - a) * r) / (b - a)) * (b + a)) / 2) - ((b - a) * (r * (a / (b - a))))) + ((c - b) * (- (((r / (c - b)) * (c + b)) / 2)))) + (((c - b) * (r * c)) / (c - b))
.= (((((((b - a) * r) / (b - a)) * (b + a)) / 2) - ((b - a) * ((r * a) / (b - a)))) + ((c - b) * (- (((r / (c - b)) * (c + b)) / 2)))) + (((c - b) * (r * c)) / (c - b)) by XCMPLX_1:74
.= (((((((b - a) * r) / (b - a)) * (b + a)) / 2) - ((b - a) * ((r * a) / (b - a)))) - ((((c - b) * (r / (c - b))) * (c + b)) / 2)) + (((c - b) * (r * c)) / (c - b))
.= (((((((b - a) * r) / (b - a)) * (b + a)) / 2) - ((b - a) * ((r * a) / (b - a)))) - (((((c - b) * r) / (c - b)) * (c + b)) / 2)) + (((c - b) * (r * c)) / (c - b)) by XCMPLX_1:74
.= ((((r * (b + a)) / 2) - ((b - a) * ((r * a) / (b - a)))) - (((((c - b) * r) / (c - b)) * (c + b)) / 2)) + (((c - b) * (r * c)) / (c - b)) by XCMPLX_1:89, A7
.= ((((r * (b + a)) / 2) - ((b - a) * ((r * a) / (b - a)))) - ((r * (c + b)) / 2)) + (((c - b) * (r * c)) / (c - b)) by XCMPLX_1:89, A7
.= ((((r * (b + a)) / 2) - ((b - a) * ((r * a) / (b - a)))) - ((r * (c + b)) / 2)) + (r * c) by XCMPLX_1:89, A7
.= ((((r * (b + a)) / 2) - (((b - a) * (r * a)) / (b - a))) - ((r * (c + b)) / 2)) + (r * c) by XCMPLX_1:74
.= ((((r * (b + a)) / 2) - (r * a)) - ((r * (c + b)) / 2)) + (r * c) by XCMPLX_1:89, A7
.= (r * (c - a)) / 2 ; :: thesis: verum