let a, b be Real; :: 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 by TAYLOR_1:2;
then #Z n is_differentiable_on REAL by A2;
then A3: ((n + 1) (#) (#Z n)) | REAL is continuous by A1, FDIFF_1:20, FDIFF_1:25;
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 4;
then (#Z (n + 1)) . a = (- (integral (((n + 1) (#) (#Z n)),a,b))) + ((#Z (n + 1)) . b) by A4, A6, A9, A10, INTEGRA5:def 4;
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