let f, P be PartFunc of REAL,REAL; :: thesis:
let x, y, a, b, s, t be Real; :: thesis:
assume A1: ( x <= y & s <= t & ['s,t'] c= ].a,b.[ ) ; :: thesis:
assume that
A2: ['x,y'] c= dom f and
A3: f is continuous and
A4: P is_differentiable_on ].a,b.[ and
A5: P .: ].a,b.[ is open Subset of REAL and
A6: P `| ].a,b.[ is continuous and
A7: P .: ].a,b.[ c= ].x,y.[ and
A8: ['s,t'] c= dom (f * P) ; :: thesis:
A9: ['x,y'] = [.x,y.] by A1, INTEGRA5:def 3;
A10: ].x,y.[ c= [.x,y.] by XXREAL_1:25;
then A11: P .: ].a,b.[ c= dom f by A7, A2, A9;
A12: ].a,b.[ c= dom P by A4;
A13: ['s,t'] = [.s,t.] by A1, INTEGRA5:def 3;
( s in [.s,t.] & t in [.s,t.] ) by A1;
then A14: ( s in ].a,b.[ & t in ].a,b.[ ) by A1, A13;
then A15: ( s in dom P & t in dom P ) by A12;
then ( P . s in P .: ].a,b.[ & P . t in P .: ].a,b.[ ) by A14, FUNCT_1:def 6;
then A16: ( P . s in ].x,y.[ & P . t in ].x,y.[ ) by A7;
f | ['x,y'] is continuous by A3;
hence ( f | ['x,y'] is bounded & f is_integrable_on ['x,y'] ) by A2, INTEGRA5:10, INTEGRA5:11; :: thesis:
consider F being PartFunc of REAL,REAL such that
A17: ( ].x,y.[ c= dom F & ( for t being Real st t in ].x,y.[ holds
F . t = integral (f,x,t) ) & ( for t being Real st t in ].x,y.[ holds
( F is_differentiable_in t & diff (F,t) = f . t ) ) ) by A1, A2, A3, Th32;
for t being Real st t in ].x,y.[ holds
F is_differentiable_in t by A17;
then F is_differentiable_on ].x,y.[ by FDIFF_1:9, A17;
then A18: F is_differentiable_on P .: ].a,b.[ by A7, A5, FDIFF_1:26;
set G = F * P;
A19: P | ].a,b.[ is continuous by A4, FDIFF_1:25;
A20: dom (F `| (P .: ].a,b.[)) = P .: ].a,b.[ by A18, FDIFF_1:def 7;
A21: dom (f | (P .: ].a,b.[)) = P .: ].a,b.[ by RELAT_1:62, A11;

now :: thesis:

let t be object ; :: thesis:
assume t in dom (F `| (P .: ].a,b.[)) ; :: thesis:
then A22: t in P .: ].a,b.[ by A20;
then reconsider s = t as Real ;
A23: s in ].x,y.[ by A22, A7;
thus (F `| (P .: ].a,b.[)) . t = diff (F,s) by A22, A18, FDIFF_1:def 7
.= f . t by A17, A23
.= (f | (P .: ].a,b.[)) . t by A22, FUNCT_1:49 ; :: thesis:

end;

now :: thesis:

end;

proof

A43: ( P . t in [.x,y.] & P . s in [.x,y.] ) by A10, A16;
then A44: ex r being Real st
( P . t = r & x <= r & r <= y ) ;
A45: ex r being Real st
( P . s = r & x <= r & r <= y ) by A43;

per cases ;

suppose A46: P . t <= P . s ; :: thesis:

then A49: x <= P . s by A44, XXREAL_0:2;
then A50: ['x,(P . s)'] = [.x,(P . s).] by INTEGRA5:def 3;
['(P . t),(P . s)'] = [.(P . t),(P . s).] by A46, INTEGRA5:def 3;
then - (integral (f,['(P . t),(P . s)'])) = integral (f,(P . s),(P . t)) by INTEGRA5:20;
then A51: integral (f,['(P . t),(P . s)']) = - (integral (f,(P . s),(P . t))) ;
[.x,(P . s).] c= [.x,y.] by A45, XXREAL_1:34;
then A52: ['x,(P . s)'] c= dom f by A2, A9, A50;
f | ['x,(P . s)'] is continuous by A3;
then A53: ( f | ['x,(P . s)'] is bounded & f is_integrable_on ['x,(P . s)'] ) by A52, INTEGRA5:10, INTEGRA5:11;
( P . t in ['x,(P . s)'] & P . s in ['x,(P . s)'] ) by A44, A45, A46, A50;
then integral (f,x,(P . s)) = (integral (f,x,(P . t))) + (integral (f,(P . t),(P . s))) by A49, A52, A53, INTEGRA6:20;
then (integral (f,x,(P . s))) - (integral (f,x,(P . t))) = - (integral (f,(P . s),(P . t))) by A51, A46, INTEGRA5:def 4;
hence (F . (P . t)) - (F . (P . s)) = integral (f,(P . s),(P . t)) by A40, A41; :: thesis:

end;

suppose A54: P . s <= P . t ; :: thesis:

then A57: x <= P . t by A45, XXREAL_0:2;
then A58: ['x,(P . t)'] = [.x,(P . t).] by INTEGRA5:def 3;
[.x,(P . t).] c= [.x,y.] by A44, XXREAL_1:34;
then A59: ['x,(P . t)'] c= dom f by A2, A9, A58;
f | ['x,(P . t)'] is continuous by A3;
then A60: ( f | ['x,(P . t)'] is bounded & f is_integrable_on ['x,(P . t)'] ) by A59, INTEGRA5:10, INTEGRA5:11;
( P . s in [.x,(P . t).] & P . t in [.x,(P . t).] ) by A44, A45, A54;
then integral (f,x,(P . t)) = (integral (f,x,(P . s))) + (integral (f,(P . s),(P . t))) by A58, A57, A59, A60, INTEGRA6:20;
hence (F . (P . t)) - (F . (P . s)) = integral (f,(P . s),(P . t)) by A40, A41; :: thesis:

end;

A61: (F * P) . s = F . (P . s) by FUNCT_1:13, A15;
A62: (F * P) . t = F . (P . t) by FUNCT_1:13, A15;
A63: integral ((((f | (P .: ].a,b.[)) * (P | ].a,b.[)) (#) (P `| ].a,b.[)),s,t) = integral (f,(P . s),(P . t)) by A38, A39, A42, A61, A62;
set K = f | (P .: ].a,b.[);
set W = (f | (P .: ].a,b.[)) * (P | ].a,b.[);
set R = ((f | (P .: ].a,b.[)) * (P | ].a,b.[)) (#) (P `| ].a,b.[);
A64: integral ((((f | (P .: ].a,b.[)) * (P | ].a,b.[)) (#) (P `| ].a,b.[)),s,t) = integral ((((f | (P .: ].a,b.[)) * (P | ].a,b.[)) (#) (P `| ].a,b.[)),['s,t']) by A1, INTEGRA5:def 4
.= integral ((((f | (P .: ].a,b.[)) * (P | ].a,b.[)) (#) (P `| ].a,b.[)) || ['s,t']) ;
A65: ((f | (P .: ].a,b.[)) * P) | ['s,t'] = (f | (P .: ].a,b.[)) * (P | ['s,t']) by RELAT_1:83;
A66: (f * P) | ['s,t'] = f * (P | ['s,t']) by RELAT_1:83;
rng (P | ['s,t']) = P .: ['s,t'] by RELAT_1:115;
then A67: rng (P | ['s,t']) c= P .: ].a,b.[ by A1, RELAT_1:123;
then A68: rng (P | ['s,t']) c= dom f by A11;
A69: ['s,t'] c= dom P by A1, A12;
A70: dom ((f * P) | ['s,t']) = dom (P | ['s,t']) by A66, A68, RELAT_1:27
.= ['s,t'] by RELAT_1:62, A69 ;
dom (f | (P .: ].a,b.[)) = P .: ].a,b.[ by RELAT_1:62, A11;
then A71: dom (((f | (P .: ].a,b.[)) * P) | ['s,t']) = dom (P | ['s,t']) by A65, A67, RELAT_1:27
.= ['s,t'] by RELAT_1:62, A69 ;

now :: thesis:

let v be object ; :: thesis:
assume v in dom ((f * P) | ['s,t']) ; :: thesis:
then A72: v in ['s,t'] by A70;
then reconsider r = v as Real ;
A73: r in dom P by A69, A72;
then A74: P . r in P .: ].a,b.[ by A1, A72, FUNCT_1:def 6;
thus ((f * P) | ['s,t']) . v = (f * P) . r by FUNCT_1:49, A72
.= f . (P . r) by A73, FUNCT_1:13
.= (f | (P .: ].a,b.[)) . (P . v) by FUNCT_1:49, A74
.= ((f | (P .: ].a,b.[)) * P) . r by FUNCT_1:13, A73
.= (((f | (P .: ].a,b.[)) * P) | ['s,t']) . v by FUNCT_1:49, A72 ; :: thesis:

end;

then A75: (f * P) | ['s,t'] = ((f | (P .: ].a,b.[)) * P) | ['s,t'] by A70, A71, FUNCT_1:2;
A76: (P | ].a,b.[) | ['s,t'] = P | ['s,t'] by A1, RELAT_1:74;
A77: (((f | (P .: ].a,b.[)) * (P | ].a,b.[)) (#) (P `| ].a,b.[)) || ['s,t'] = (((f | (P .: ].a,b.[)) * (P | ].a,b.[)) | ['s,t']) (#) ((P `| ].a,b.[) | ['s,t']) by RFUNCT_1:45
.= ((f | (P .: ].a,b.[)) * ((P | ].a,b.[) | ['s,t'])) (#) ((P `| ].a,b.[) | ['s,t']) by RELAT_1:83
.= (((f | (P .: ].a,b.[)) * P) | ['s,t']) (#) ((P `| ].a,b.[) | ['s,t']) by A76, RELAT_1:83
.= ((f * P) (#) (P `| ].a,b.[)) || ['s,t'] by A75, RFUNCT_1:45 ;
hence A78: ((f * P) (#) (P `| ].a,b.[)) | ['s,t'] is continuous by A37, A35, A24, A34; :: thesis:
dom (P `| ].a,b.[) = ].a,b.[ by A4, FDIFF_1:def 7;
then A79: dom ((f * P) (#) (P `| ].a,b.[)) = (dom (f * P)) /\ ].a,b.[ by VALUED_1:def 4;
['s,t'] /\ ].a,b.[ c= (dom (f * P)) /\ ].a,b.[ by XBOOLE_1:26, A8;
hence ['s,t'] c= dom ((f * P) (#) (P `| ].a,b.[)) by A1, A79, XBOOLE_1:28; :: thesis:
hence ( ((f * P) (#) (P `| ].a,b.[)) | ['s,t'] is bounded & (f * P) (#) (P `| ].a,b.[) is_integrable_on ['s,t'] ) by A78, INTEGRA5:10, INTEGRA5:11; :: thesis:
integral ((((f | (P .: ].a,b.[)) * (P | ].a,b.[)) (#) (P `| ].a,b.[)) || ['s,t']) = integral (((f * P) (#) (P `| ].a,b.[)),['s,t']) by A77
.= integral (((f * P) (#) (P `| ].a,b.[)),s,t) by A1, INTEGRA5:def 4 ;
hence integral (((f * P) (#) (P `| ].a,b.[)),s,t) = integral (f,(P . s),(P . t)) by A63, A64; :: thesis: