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_{1}( 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_{1}(x)
from FUNCT_2:sch 4();

a6: for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L

.= 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

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

consider g being Function of REAL,REAL such that

A6: for x being Element of REAL holds g . x = H

a6: for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L

proof

then A8:
g is_differentiable_on REAL
by Lm4, FUNCT_2:def 1;
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;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

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

(g `| ([#] REAL)) . x = (f0 | ([#] REAL)) . x

dom (g `| ([#] REAL)) =
[#] REAL
by A8, FDIFF_1:def 7
(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;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

.= 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