let n be non zero Element of NAT ; :: thesis: for a, r, t, L being Real
for f0 being Function of REAL,REAL st a <= t & ( for x being Real holds f0 . x = r * ((((r * (x - a)) |^ n) / (n !)) * L) ) holds
( f0 | [.a,t.] is continuous & f0 | [.a,t.] is bounded & f0 is_integrable_on ['a,t'] & integral (f0,a,t) = (((r * (t - a)) |^ (n + 1)) / ((n + 1) !)) * L )
let a, r, t, L be Real; :: thesis: for f0 being Function of REAL,REAL st a <= t & ( for x being Real holds f0 . x = r * ((((r * (x - a)) |^ n) / (n !)) * L) ) holds
( f0 | [.a,t.] is continuous & f0 | [.a,t.] is bounded & f0 is_integrable_on ['a,t'] & integral (f0,a,t) = (((r * (t - a)) |^ (n + 1)) / ((n + 1) !)) * L )
let f0 be Function of REAL,REAL; :: thesis: ( a <= t & ( for x being Real holds f0 . x = r * ((((r * (x - a)) |^ n) / (n !)) * L) ) implies ( f0 | [.a,t.] is continuous & f0 | [.a,t.] is bounded & f0 is_integrable_on ['a,t'] & integral (f0,a,t) = (((r * (t - a)) |^ (n + 1)) / ((n + 1) !)) * L ) )
S: a in REAL by XREAL_0:def 1;
assume A1: a <= t ; :: thesis: ( ex x being Real st not f0 . x = r * ((((r * (x - a)) |^ n) / (n !)) * L) or ( f0 | [.a,t.] is continuous & f0 | [.a,t.] is bounded & f0 is_integrable_on ['a,t'] & integral (f0,a,t) = (((r * (t - a)) |^ (n + 1)) / ((n + 1) !)) * L ) )
assume A2: for x being Real holds f0 . x = r * ((((r * (x - a)) |^ n) / (n !)) * L) ; :: thesis: ( f0 | [.a,t.] is continuous & f0 | [.a,t.] is bounded & f0 is_integrable_on ['a,t'] & integral (f0,a,t) = (((r * (t - a)) |^ (n + 1)) / ((n + 1) !)) * L )
A5: dom f0 = REAL by FUNCT_2:def 1;
for x being Real st x in dom f0 holds
f0 is_continuous_in x by A2, Lm5, FDIFF_1:24;
then reconsider f0 = f0 as continuous PartFunc of REAL,REAL by FCONT_1:def 2;
deffunc H₁( Real) -> Element of REAL = In (((((r * ($1 - a)) |^ (n + 1)) / ((n + 1) !)) * L),REAL);
consider g being Function of REAL,REAL such that
A6: for x being Element of REAL holds g . x = H₁(x) from FUNCT_2:sch 4();
a6: for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L

proof

let x be Real; :: thesis: g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L
x in REAL by XREAL_0:def 1;
then g . x = In (((((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L),REAL) by A6;
hence g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L ; :: thesis: verum

end;

then A8: g is_differentiable_on REAL by Lm4, FUNCT_2:def 1;

A9: now :: thesis: for x being Element of REAL st x in dom (g `| ([#] REAL)) holds
(g `| ([#] REAL)) . x = (f0 | ([#] REAL)) . x

let x be Element of REAL ; :: thesis: ( x in dom (g `| ([#] REAL)) implies (g `| ([#] REAL)) . x = (f0 | ([#] REAL)) . x )
assume x in dom (g `| ([#] REAL)) ; :: thesis: (g `| ([#] REAL)) . x = (f0 | ([#] REAL)) . x
thus (g `| ([#] REAL)) . x = diff (g,x) by A8, FDIFF_1:def 7
.= r * ((((r * (x - a)) |^ n) / (n !)) * L) by Lm4, a6
.= (f0 | ([#] REAL)) . x by A2 ; :: thesis: verum

end;

dom (g `| ([#] REAL)) = [#] REAL by A8, FDIFF_1:def 7
.= dom (f0 | ([#] REAL)) by FUNCT_2:def 1 ;
then g `| ([#] REAL) = f0 | ([#] REAL) by A9, PARTFUN1:5;
then g in IntegralFuncs (f0,([#] REAL)) by A8, INTEGRA7:def 1;
then A10: g is_integral_of f0, [#] REAL by INTEGRA7:def 2;
A11: f0 | ['a,t'] is bounded by INTEGRA5:10, A5;
A12: g . t = (integral (f0,a,t)) + (g . a) by A1, INTEGRA7:18, A5, INTEGRA5:11, A11, A10;
A13: 0 + 1 <= n + 1 by XREAL_1:6;
g . a = In (((((r * (a - a)) |^ (n + 1)) / ((n + 1) !)) * L),REAL) by A6, S
.= (0 / ((n + 1) !)) * L by A13, NEWTON:11
.= 0 ;
hence ( f0 | [.a,t.] is continuous & f0 | [.a,t.] is bounded & f0 is_integrable_on ['a,t'] & integral (f0,a,t) = (((r * (t - a)) |^ (n + 1)) / ((n + 1) !)) * L ) by A11, A12, A5, INTEGRA5:11, a6, A1, INTEGRA5:def 3; :: thesis: verum