let b, a be real number ; :: thesis: for n being Element of NAT holds ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b
let n be Element of NAT ; :: thesis: ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b
A1: [#] REAL c= dom ((n + 1) (#) (#Z n)) by FUNCT_2:def 1;
A2: dom (#Z n) = REAL by FUNCT_2:def 1;
for x being Real st x in REAL holds
(#Z n) | REAL is_differentiable_in x

proof

let x be Real; :: thesis: ( x in REAL implies (#Z n) | REAL is_differentiable_in x )
assume x in REAL ; :: thesis: (#Z n) | REAL is_differentiable_in x
#Z n is_differentiable_in x by TAYLOR_1:2;
hence (#Z n) | REAL is_differentiable_in x by A2, RELAT_1:97; :: thesis: verum

end;

then #Z n is_differentiable_on REAL by A2, FDIFF_1:def 7;
then A3: ((n + 1) (#) (#Z n)) | REAL is continuous by A1, FDIFF_1:28, FDIFF_1:33;
A4: min a,b <= a by XXREAL_0:17;
A5: [.(min a,b),(max a,b).] c= REAL ;
a <= max a,b by XXREAL_0:25;
then min a,b <= max a,b by A4, XXREAL_0:2;
then A6: (#Z (n + 1)) . (max a,b) = (integral ((n + 1) (#) (#Z n)),(min a,b),(max a,b)) + ((#Z (n + 1)) . (min a,b)) by A1, A3, A5, Th20, Th29;
A7: ( min a,b = a implies ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b )

proof

assume A8: min a,b = a ; :: thesis: ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b
then max a,b = b by XXREAL_0:36;
hence ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b by A6, A8; :: thesis: verum

end;

( min a,b = b implies ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b )

proof

assume A9: min a,b = b ; :: thesis: ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b
then A10: max a,b = a by XXREAL_0:36;
( b < a implies ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b )

proof

assume b < a ; :: thesis: ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b
then integral ((n + 1) (#) (#Z n)),a,b = - (integral ((n + 1) (#) (#Z n)),['b,a']) by INTEGRA5:def 5;
then (#Z (n + 1)) . a = (- (integral ((n + 1) (#) (#Z n)),a,b)) + ((#Z (n + 1)) . b) by A4, A6, A9, A10, INTEGRA5:def 5;
hence ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b ; :: thesis: verum

end;

hence ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b by A4, A7, A9, XXREAL_0:1; :: thesis: verum

end;

hence ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral ((n + 1) (#) (#Z n)),a,b by A7, XXREAL_0:15; :: thesis: verum