let a, t, L, r be Real; :: thesis: for k being non zero Element of NAT st a <= t holds
ex rg being PartFunc of REAL,REAL st
( dom rg = [.a,t.] & ( for x being Real st x in [.a,t.] holds
rg . x = r * ((((r * (x - a)) |^ k) / (k !)) * L) ) & rg is continuous & rg is_integrable_on ['a,t'] & rg | [.a,t.] is bounded & integral (rg,a,t) = (((r * (t - a)) |^ (k + 1)) / ((k + 1) !)) * L )
let k be non zero Element of NAT ; :: thesis: ( a <= t implies ex rg being PartFunc of REAL,REAL st
( dom rg = [.a,t.] & ( for x being Real st x in [.a,t.] holds
rg . x = r * ((((r * (x - a)) |^ k) / (k !)) * L) ) & rg is continuous & rg is_integrable_on ['a,t'] & rg | [.a,t.] is bounded & integral (rg,a,t) = (((r * (t - a)) |^ (k + 1)) / ((k + 1) !)) * L ) )
assume A1: a <= t ; :: thesis: ex rg being PartFunc of REAL,REAL st
( dom rg = [.a,t.] & ( for x being Real st x in [.a,t.] holds
rg . x = r * ((((r * (x - a)) |^ k) / (k !)) * L) ) & rg is continuous & rg is_integrable_on ['a,t'] & rg | [.a,t.] is bounded & integral (rg,a,t) = (((r * (t - a)) |^ (k + 1)) / ((k + 1) !)) * L )
then X1: ['a,t'] = [.a,t.] by INTEGRA5:def 3;
deffunc H₁( Real) -> Element of REAL = In ((r * ((((r * ($1 - a)) |^ k) / (k !)) * L)),REAL);
consider f0 being Function of REAL,REAL such that
A2: for x being Element of REAL holds f0 . x = H₁(x) from FUNCT_2:sch 4();
a2: for x being Real holds f0 . x = r * ((((r * (x - a)) |^ k) / (k !)) * L)

proof

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

end;

A3: dom f0 = REAL by FUNCT_2:def 1;
A4: ( f0 | [.a,t.] is continuous & f0 | [.a,t.] is bounded & f0 is_integrable_on ['a,t'] & integral (f0,a,t) = (((r * (t - a)) |^ (k + 1)) / ((k + 1) !)) * L ) by Lm6, A1, a2;
set f = f0 | [.a,t.];
reconsider f = f0 | [.a,t.] as continuous PartFunc of REAL,REAL by Lm6, A1, a2;

A7: now :: thesis: for x being Real st x in [.a,t.] holds
f . x = r * ((((r * (x - a)) |^ k) / (k !)) * L)

let x be Real; :: thesis: ( x in [.a,t.] implies f . x = r * ((((r * (x - a)) |^ k) / (k !)) * L) )
assume A8: x in [.a,t.] ; :: thesis: f . x = r * ((((r * (x - a)) |^ k) / (k !)) * L)
A9: x in REAL by XREAL_0:def 1;
thus f . x = f0 . x by A8, FUNCT_1:49
.= In ((r * ((((r * (x - a)) |^ k) / (k !)) * L)),REAL) by A2, A9
.= r * ((((r * (x - a)) |^ k) / (k !)) * L) ; :: thesis: verum

end;

A10: ( integral (f0,a,t) = integral (f0,['a,t']) & integral (f,a,t) = integral (f,['a,t']) ) by INTEGRA5:def 4, A1;
take f ; :: thesis: ( dom f = [.a,t.] & ( for x being Real st x in [.a,t.] holds
f . x = r * ((((r * (x - a)) |^ k) / (k !)) * L) ) & f is continuous & f is_integrable_on ['a,t'] & f | [.a,t.] is bounded & integral (f,a,t) = (((r * (t - a)) |^ (k + 1)) / ((k + 1) !)) * L )
thus ( dom f = [.a,t.] & ( for x being Real st x in [.a,t.] holds
f . x = r * ((((r * (x - a)) |^ k) / (k !)) * L) ) & f is continuous & f is_integrable_on ['a,t'] & f | [.a,t.] is bounded & integral (f,a,t) = (((r * (t - a)) |^ (k + 1)) / ((k + 1) !)) * L ) by A7, A10, A4, A3, X1, RELAT_1:62; :: thesis: verum