let a, b, p, q be Real; for f, g being PartFunc of REAL,REAL st a < b & p < q & [.a,b.] c= dom f & f | ['a,b'] is continuous & g is_differentiable_on_interval ['p,q'] & g `\ ['p,q'] is_integrable_on ['p,q'] & g `\ ['p,q'] is bounded & rng (g | ['p,q']) c= ['a,b'] & g . p = a & g . q = b holds
integral (f,a,b) = integral (((f * g) (#) (g `\ ['p,q'])),p,q)
let f, g be PartFunc of REAL,REAL; ( a < b & p < q & [.a,b.] c= dom f & f | ['a,b'] is continuous & g is_differentiable_on_interval ['p,q'] & g `\ ['p,q'] is_integrable_on ['p,q'] & g `\ ['p,q'] is bounded & rng (g | ['p,q']) c= ['a,b'] & g . p = a & g . q = b implies integral (f,a,b) = integral (((f * g) (#) (g `\ ['p,q'])),p,q) )
assume that
A1:
a < b
and
A2:
p < q
and
A3:
[.a,b.] c= dom f
and
A4:
f | ['a,b'] is continuous
and
A5:
g is_differentiable_on_interval ['p,q']
and
A6:
g `\ ['p,q'] is_integrable_on ['p,q']
and
A7:
g `\ ['p,q'] is bounded
and
A8:
rng (g | ['p,q']) c= ['a,b']
and
A9:
g . p = a
and
A10:
g . q = b
; integral (f,a,b) = integral (((f * g) (#) (g `\ ['p,q'])),p,q)
A11:
( ['a,b'] = [.a,b.] & ['p,q'] = [.p,q.] )
by A1, A2, INTEGRA5:def 3;
reconsider I = ['a,b'], J = ['p,q'] as non empty closed_interval Subset of REAL ;
consider F being PartFunc of REAL,REAL such that
A12:
( dom F = REAL & ( for x being Real st x in I holds
F . x = integral (f,a,x) ) )
by Lm1;
A13:
( F is_differentiable_on_interval I & F `\ I = f | I )
by A1, A11, A4, A3, A12, Th37;
A14:
g .: J = rng (g | J)
by RELAT_1:115;
then A15:
( F * g is_differentiable_on_interval J & (F * g) `\ J = ((F `\ I) * g) (#) (g `\ J) )
by A8, A13, A5, FDIFF_12:52;
A16:
g | J is continuous
by A5, FDIFF_12:37;
A17:
J c= dom g
by A5, FDIFF_12:def 1;
A18:
dom (f | I) = I
by A3, A11, RELAT_1:62;
then A19:
J c= dom ((f | I) * g)
by A8, A14, A17, FUNCT_1:101;
A20:
J = dom (g `\ J)
by A5, FDIFF_12:def 2;
then A21:
(g `\ J) | J = g `\ J
;
A22:
(g `\ J) | J is bounded
by A7;
(f | I) * (g | J) is continuous
by A4, A16;
then
((f | I) * g) | J is continuous
by RELAT_1:83;
then A23:
((f | I) * g) | J is bounded
by A19, INTEGRA5:10;
then
(((f | I) * g) (#) (g `\ J)) | (J /\ J) is bounded
by A22, RFUNCT_1:84;
then A24:
(F * g) `\ J is bounded
by A13, A15, A21, RFUNCT_1:45;
(f | I) | (g .: J) is continuous
by A4;
then
(f | I) * g is_integrable_on J
by A19, A16, FCONT_1:25, INTEGRA5:11;
then A25:
integral ((((f | I) * g) (#) (g `\ J)),J) = ((F * g) . q) - ((F * g) . p)
by A6, A19, A20, A23, A7, A13, A2, A15, A24, Lm4, INTEGRA6:14;
f is_integrable_on I
by A3, A4, A11, INTEGRA5:11;
then A26:
f | I is_integrable_on I
;
integral ((f | I),I) = (F . b) - (F . a)
by A3, A4, A11, A1, A26, A13, Lm4, INTEGRA5:10;
then A27:
integral (f,I) = (F . b) - (F . a)
;
(f | I) * (g | J) = f * (g | J)
by A18, A8, RELAT_1:165;
then A28:
((f | I) * g) | J = f * (g | J)
by RELAT_1:83;
integral ((((f | I) * g) (#) (g `\ J)),J) =
integral (((((f | I) * g) (#) (g `\ J)) | J) || J)
.=
integral (((((f | I) * g) | J) (#) (g `\ J)) || J)
by RFUNCT_1:45
.=
integral ((((f * g) | J) (#) (g `\ J)) || J)
by A28, RELAT_1:83
.=
integral ((((f * g) (#) (g `\ J)) | J) || J)
by RFUNCT_1:45
;
then A29:
integral ((((f | I) * g) (#) (g `\ J)),J) = integral (((f * g) (#) (g `\ J)),J)
;
( p in dom g & q in dom g )
by A11, A17, A2, XXREAL_1:1;
then
( (F * g) . q = F . b & (F * g) . p = F . a )
by A9, A10, FUNCT_1:13;
then
integral ((((f | I) * g) (#) (g `\ J)),J) = integral (f,a,b)
by A27, A11, A25, INTEGRA5:19;
hence
integral (f,a,b) = integral (((f * g) (#) (g `\ ['p,q'])),p,q)
by A11, A29, INTEGRA5:19; verum