let a, b be Real; :: thesis: for n being Element of NAT
for A being non empty closed_interval Subset of REAL st a * (n + 1) <> 0 holds
integral (((#Z n) * (AffineMap (a,b))),A) = (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (upper_bound A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (lower_bound A))
let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL st a * (n + 1) <> 0 holds
integral (((#Z n) * (AffineMap (a,b))),A) = (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (upper_bound A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; :: thesis: ( a * (n + 1) <> 0 implies integral (((#Z n) * (AffineMap (a,b))),A) = (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (upper_bound A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (lower_bound A)) )
assume A1: a * (n + 1) <> 0 ; :: thesis: integral (((#Z n) * (AffineMap (a,b))),A) = (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (upper_bound A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (lower_bound A))
A2: [#] REAL = dom (AffineMap (a,b)) by FUNCT_2:def 1;
A3: for x being Element of REAL st x in dom (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) holds
(((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((#Z n) * (AffineMap (a,b))) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) implies (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((#Z n) * (AffineMap (a,b))) . x )
assume x in dom (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) ; :: thesis: (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((#Z n) * (AffineMap (a,b))) . x
(((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n by A1, Th12
.= ((AffineMap (a,b)) . x) #Z n by FCONT_1:def 4
.= (#Z n) . ((AffineMap (a,b)) . x) by TAYLOR_1:def 1
.= ((#Z n) * (AffineMap (a,b))) . x by A2, FUNCT_1:13 ;
hence (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((#Z n) * (AffineMap (a,b))) . x ; :: thesis: verum

end;

A4: [#] REAL = dom ((#Z n) * (AffineMap (a,b))) by FUNCT_2:def 1;
for x being Real st x in REAL holds
(AffineMap (a,b)) . x = (a * x) + b by FCONT_1:def 4;
then A5: AffineMap (a,b) is_differentiable_on REAL by A2, FDIFF_1:23;
for x being Real holds (#Z n) * (AffineMap (a,b)) is_differentiable_in x

proof

let x be Real; :: thesis: (#Z n) * (AffineMap (a,b)) is_differentiable_in x
x in REAL by XREAL_0:def 1;
then AffineMap (a,b) is_differentiable_in x by A2, A5, FDIFF_1:9;
hence (#Z n) * (AffineMap (a,b)) is_differentiable_in x by TAYLOR_1:3; :: thesis: verum

end;

then for x being Real st x in REAL holds
(#Z n) * (AffineMap (a,b)) is_differentiable_in x ;
then (#Z n) * (AffineMap (a,b)) is_differentiable_on REAL by A4, FDIFF_1:9;
then A6: ((#Z n) * (AffineMap (a,b))) | REAL is continuous by FDIFF_1:25;
then ((#Z n) * (AffineMap (a,b))) | A is continuous by FCONT_1:16;
then A7: (#Z n) * (AffineMap (a,b)) is_integrable_on A by A4, INTEGRA5:11;
(1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b))) is_differentiable_on REAL by A1, Th12;
then dom (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) = dom ((#Z n) * (AffineMap (a,b))) by A4, FDIFF_1:def 7;
then A8: ((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL = (#Z n) * (AffineMap (a,b)) by A3, PARTFUN1:5;
((#Z n) * (AffineMap (a,b))) | A is bounded by A4, A6, INTEGRA5:10;
hence integral (((#Z n) * (AffineMap (a,b))),A) = (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (upper_bound A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (lower_bound A)) by A1, A7, A8, Th12, INTEGRA5:13; :: thesis: verum