let a, b, c, d be Real; ( c <= d implies integral (((id REAL) (#) (AffineMap (a,b))),c,d) = (((1 / 3) * a) * (((d * d) * d) - ((c * c) * c))) + (((1 / 2) * b) * ((d * d) - (c * c))) )
assume A1:
c <= d
; integral (((id REAL) (#) (AffineMap (a,b))),c,d) = (((1 / 3) * a) * (((d * d) * d) - ((c * c) * c))) + (((1 / 2) * b) * ((d * d) - (c * c)))
reconsider D = ['c,d'] as non empty closed_interval Subset of REAL ;
reconsider F2 = #Z 2 as PartFunc of REAL,REAL ;
reconsider F1 = #Z 1 as PartFunc of REAL,REAL ;
DD:
['c,d'] c= REAL
;
B2:
['c,d'] c= dom (#Z 2)
by FUNCT_2:def 1, DD;
B3:
D c= dom F1
by FUNCT_2:def 1, DD;
F1 | D is continuous
;
then B4:
( F1 is_integrable_on D & F1 | ['c,d'] is bounded )
by INTEGRA5:10, INTEGRA5:11, B3;
F2 | D is continuous
;
then B5:
( F2 is_integrable_on ['c,d'] & F2 | ['c,d'] is bounded )
by INTEGRA5:10, INTEGRA5:11, B2;
A2:
['c,d'] c= dom (a (#) F2)
by FUNCT_2:def 1, DD;
A3:
['c,d'] c= dom (b (#) F1)
by FUNCT_2:def 1, DD;
( (a (#) F2) | D is continuous & (b (#) F1) | D is continuous )
;
then A4:
( b (#) F1 is_integrable_on ['c,d'] & a (#) F2 is_integrable_on ['c,d'] & (b (#) F1) | ['c,d'] is bounded & (a (#) F2) | ['c,d'] is bounded )
by INTEGRA5:10, INTEGRA5:11, A2, A3;
( [.(lower_bound ['c,d']),(upper_bound ['c,d']).] = ['c,d'] & ['c,d'] = [.c,d.] )
by A1, INTEGRA5:def 3, INTEGRA1:4;
then LM:
( lower_bound D = c & d = upper_bound D )
by INTEGRA1:5;
integral (((id REAL) (#) (AffineMap (a,b))),c,d) =
integral (((a (#) (#Z 2)) + (b (#) (#Z 1))),c,d)
by Th23C
.=
(integral ((a (#) F2),c,d)) + (integral ((b (#) F1),c,d))
by INTEGRA6:12, A1, A2, A3, A4
.=
(a * (integral (F2,c,d))) + (integral ((b (#) F1),c,d))
by INTEGRA6:10, A1, B2, B5
.=
(a * (integral (F2,c,d))) + (b * (integral (F1,c,d)))
by INTEGRA6:10, A1, B3, B4
.=
(a * (integral (F2,D))) + (b * (integral (F1,c,d)))
by INTEGRA5:def 4, A1
.=
(a * (integral (F2,D))) + (b * (integral (F1,D)))
by INTEGRA5:def 4, A1
.=
(a * (((1 / (2 + 1)) * ((upper_bound D) |^ (2 + 1))) - ((1 / (2 + 1)) * ((lower_bound D) |^ (2 + 1))))) + (b * (integral (F1,D)))
by INTEGRA9:19
.=
(a * (((1 / 3) * (d |^ (2 + 1))) - ((1 / 3) * (c |^ (2 + 1))))) + (b * (((1 / 2) * (d |^ (1 + 1))) - ((1 / 2) * (c |^ (1 + 1)))))
by LM, INTEGRA9:19
.=
((a * (1 / 3)) * ((d |^ (2 + 1)) - (c |^ (2 + 1)))) + ((b * (1 / 2)) * ((d |^ (1 + 1)) - (c |^ (1 + 1))))
.=
((a * (1 / 3)) * (((d |^ 2) * d) - (c |^ (2 + 1)))) + ((b * (1 / 2)) * ((d |^ (1 + 1)) - (c |^ (1 + 1))))
by NEWTON:6
.=
((a * (1 / 3)) * (((d |^ (1 + 1)) * d) - ((c |^ 2) * c))) + ((b * (1 / 2)) * ((d |^ (1 + 1)) - (c |^ (1 + 1))))
by NEWTON:6
.=
((a * (1 / 3)) * (((d |^ (1 + 1)) * d) - ((c |^ 2) * c))) + ((b * (1 / 2)) * (((d |^ 1) * d) - (c |^ (1 + 1))))
by NEWTON:6
.=
((a * (1 / 3)) * (((d |^ (1 + 1)) * d) - ((c |^ 2) * c))) + ((b * (1 / 2)) * ((d * d) - ((c |^ 1) * c)))
by NEWTON:6
.=
((a * (1 / 3)) * ((((d |^ 1) * d) * d) - ((c |^ (1 + 1)) * c))) + ((b * (1 / 2)) * ((d * d) - (c * c)))
by NEWTON:6
.=
((a * (1 / 3)) * (((d * d) * d) - (((c |^ 1) * c) * c))) + ((b * (1 / 2)) * ((d * d) - (c * c)))
by NEWTON:6
;
hence
integral (((id REAL) (#) (AffineMap (a,b))),c,d) = (((1 / 3) * a) * (((d * d) * d) - ((c * c) * c))) + (((1 / 2) * b) * ((d * d) - (c * c)))
; verum