let a, b be Real; :: thesis: for n being Element of NAT
for A being 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 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 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 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 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 JORDAN16:def 3
.= (#Z n) . ((AffineMap a,b) . x) by TAYLOR_1:def 1
.= ((#Z n) * (AffineMap a,b)) . x by A2, FUNCT_1:23 ;
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 JORDAN16:def 3;
then A5: AffineMap a,b is_differentiable_on REAL by A2, FDIFF_1:31;
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
AffineMap a,b is_differentiable_in x by A2, A5, FDIFF_1:16;
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:16;
then A6: ((#Z n) * (AffineMap a,b)) | REAL is continuous by FDIFF_1:33;
then ((#Z n) * (AffineMap a,b)) | A is continuous by FCONT_1:17;
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 8;
then A8: ((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) `| REAL = (#Z n) * (AffineMap a,b) by A3, PARTFUN1:34;
((#Z n) * (AffineMap a,b)) | A is bounded by A4, A6, FCONT_1:17, 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