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 ) )
A1: a in REAL by XREAL_0:def 1;
assume A2: 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 A3: 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 )
A4: dom f0 = REAL by FUNCT_2:def 1;
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 A3, Lm10, 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();
A7: 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;

A8: dom g = [#] REAL by FUNCT_2:def 1;
for x being Real st x in [#] REAL holds
g is_differentiable_in x by A7, Lm9;
then A9: g is_differentiable_on REAL by A8;

A10: 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 A9, FDIFF_1:def 7
.= r * ((((r * (x - a)) |^ n) / (n !)) * L) by Lm9, A7
.= f0 . x by A3
.= (f0 | ([#] REAL)) . x ; :: thesis: verum

end;

dom (g `| ([#] REAL)) = [#] REAL by A9, FDIFF_1:def 7
.= dom (f0 | ([#] REAL)) by A4 ;
then g `| ([#] REAL) = f0 | ([#] REAL) by A10, PARTFUN1:5;
then g in IntegralFuncs (f0,([#] REAL)) by A9, INTEGRA7:def 1;
then A11: g is_integral_of f0, [#] REAL by INTEGRA7:def 2;
A12: f0 | ['a,t'] is bounded by INTEGRA5:10, A5;
A13: g . t = (integral (f0,a,t)) + (g . a) by A2, INTEGRA7:18, A5, INTEGRA5:11, A12, A11;
A14: 0 + 1 <= n + 1 by XREAL_1:6;
g . a = In (((((r * (a - a)) |^ (n + 1)) / ((n + 1) !)) * L),REAL) by A6, A1
.= (0 / ((n + 1) !)) * L by A14, 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 A12, A13, A5, INTEGRA5:11, A7; :: thesis: verum