let a, t, L, r be Real; 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 ; ( 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
; 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 H1( 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 = H1(x)
from FUNCT_2:sch 4();
A3:
for x being Real holds f0 . x = r * ((((r * (x - a)) |^ k) / (k !)) * L)
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;
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
; ( 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; verum