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 ;
then reconsider f0 = f0 as continuous PartFunc of REAL,REAL by FCONT_1:def 2;
deffunc H1( 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 = H1(x) from 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 ;
A9: now :: thesis: for x being Element of REAL st x in dom (g `| ()) holds
(g `| ()) . x = (f0 | ()) . x
let x be Element of REAL ; :: thesis: ( x in dom (g `| ()) implies (g `| ()) . x = (f0 | ()) . x )
assume x in dom (g `| ()) ; :: thesis: (g `| ()) . x = (f0 | ()) . x
thus (g `| ()) . x = diff (g,x) by
.= r * ((((r * (x - a)) |^ n) / (n !)) * L) by
.= (f0 | ()) . x by A2 ; :: thesis: verum
end;
dom (g `| ()) = [#] REAL by
.= dom (f0 | ()) by FUNCT_2:def 1 ;
then g `| () = f0 | () by ;
then g in IntegralFuncs (f0,()) by ;
then A10: g is_integral_of f0, [#] REAL by INTEGRA7:def 2;
A11: f0 | ['a,t'] is bounded by ;
A12: g . t = (integral (f0,a,t)) + (g . a) by ;
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
.= 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 ; :: thesis: verum