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))) . (sup A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) . (inf 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))) . (sup A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) . (inf 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))) . (sup A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) . (inf A)) )
assume C: a * (n + 1) <> 0 ; :: thesis: integral ((#Z n) * (AffineMap a,b)),A = (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) . (sup A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) . (inf A))
A1: ( [#] REAL = dom ((#Z n) * (AffineMap a,b)) & [#] REAL = dom ((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) & [#] REAL = dom (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 B1: ( AffineMap a,b is_differentiable_on REAL & ( for x being Real st x in [#] REAL holds
((AffineMap a,b) `| REAL ) . x = a ) ) by A1, FDIFF_1:31;
A: 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 B1, FDIFF_1:16;
hence (#Z n) * (AffineMap a,b) is_differentiable_in x by TAYLOR_1:3; :: thesis: verum

end;

A2: (#Z n) * (AffineMap a,b) is_differentiable_on REAL

proof

for x being Real st x in REAL holds
(#Z n) * (AffineMap a,b) is_differentiable_in x by A;
hence (#Z n) * (AffineMap a,b) is_differentiable_on REAL by A1, FDIFF_1:16; :: thesis: verum

end;

((#Z n) * (AffineMap a,b)) | REAL is continuous by A2, FDIFF_1:33;
then ((#Z n) * (AffineMap a,b)) | A is continuous by FCONT_1:17;
then A3: ( (#Z n) * (AffineMap a,b) is_integrable_on A & ((#Z n) * (AffineMap a,b)) | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A4: 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 C, 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 A1, 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;

(1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b)) is_differentiable_on REAL by C, Th12;
then dom (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) `| REAL ) = dom ((#Z n) * (AffineMap a,b)) by A1, FDIFF_1:def 8;
then ((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) `| REAL = (#Z n) * (AffineMap a,b) by A4, PARTFUN1:34;
hence integral ((#Z n) * (AffineMap a,b)),A = (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) . (sup A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) . (inf A)) by C, A3, Th12, INTEGRA5:13; :: thesis: verum