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 )
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();
A3: 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;

A4: dom f0 = REAL by FUNCT_2:def 1;
A5: ( 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 Lm11, A1, A3;
set f = f0 | ['a,t'];
A6: dom (f0 | ['a,t']) = ['a,t'] by A4, RELAT_1:62;
reconsider f = f0 | ['a,t'] as continuous PartFunc of REAL,REAL by Lm11, A1, A3;

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']) by INTEGRA5:def 4, A1
.= integral (f0 || ['a,t']) ;
A11: integral (f,a,t) = integral (f,['a,t']) by INTEGRA5:def 4, A1
.= integral (f || ['a,t']) ;
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, A11, A10, A5, A6; :: thesis: verum