let a, b, c, d be Real; ( c <= d implies integral ((AffineMap (a,b)),c,d) = (((1 / 2) * a) * ((d * d) - (c * c))) + (b * (d - c)) )
assume A1:
c <= d
; integral ((AffineMap (a,b)),c,d) = (((1 / 2) * a) * ((d * d) - (c * c))) + (b * (d - c))
reconsider D = ['c,d'] as non empty closed_interval Subset of REAL ;
reconsider F2 = #Z 1 as PartFunc of REAL,REAL ;
reconsider F1 = #Z 0 as PartFunc of REAL,REAL ;
DD:
['c,d'] c= REAL
;
B2:
['c,d'] c= dom (#Z 1)
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 ((AffineMap (a,b)),c,d) =
integral (((a (#) (#Z 1)) + (b (#) (#Z 0))),c,d)
by Th23E
.=
(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 / (1 + 1)) * ((upper_bound D) |^ (1 + 1))) - ((1 / (1 + 1)) * ((lower_bound D) |^ (1 + 1))))) + (b * (integral (F1,D)))
by INTEGRA9:19
.=
(a * (((1 / 2) * ((upper_bound D) |^ (1 + 1))) - ((1 / 2) * ((lower_bound D) |^ (1 + 1))))) + (b * (((1 / (0 + 1)) * ((upper_bound D) |^ (0 + 1))) - ((1 / (0 + 1)) * ((lower_bound D) |^ (0 + 1)))))
by INTEGRA9:19
.=
((a * (1 / 2)) * ((d |^ (1 + 1)) - (c |^ (1 + 1)))) + (b * ((d |^ 1) - (c |^ 1)))
by LM
.=
((a * (1 / 2)) * (((d |^ 1) * d) - (c |^ (1 + 1)))) + (b * ((d |^ 1) - (c |^ 1)))
by NEWTON:6
.=
((a * (1 / 2)) * ((d * d) - (c * c))) + (b * (d - c))
by NEWTON:6
;
hence
integral ((AffineMap (a,b)),c,d) = (((1 / 2) * a) * ((d * d) - (c * c))) + (b * (d - c))
; verum