let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL
for I, J being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J & x0 = sup I & x0 in I holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: for I, J being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J & x0 = sup I & x0 in I holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )
let I, J be non empty Interval; :: thesis: ( f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J & x0 = sup I & x0 in I implies ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 ) )
assume that
A1: f1 is_differentiable_on_interval I and
A2: f2 is_differentiable_on_interval J and
A3: f1 .: I c= J and
A4: x0 = sup I and
A5: x0 in I ; :: thesis: ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )
A6: x0 = upper_bound I by A4, A5, Lm6;
sup I = upper_bound I by A4, A5, Lm6;
then A7: f1 | I is_left_differentiable_in upper_bound I by A1, A4, A5, Th11;
then consider R1 being Real such that
A8: ( R1 > 0 & [.(x0 - R1),x0.] c= dom (f1 | I) ) by A6, FDIFF_3:def 4;
A9: f1 . x0 = (f1 | I) . x0 by A5, FUNCT_1:49;
A10: f1 . x0 in f1 .: I by A5, A1, FUNCT_1:def 6;
then f1 . x0 in J by A3;
then A11: (f1 | I) . x0 in J by A5, FUNCT_1:49;
set F1 = (f1 | I) | (left_closed_halfline x0);
x0 in ].-infty,x0.] by XXREAL_1:234;
then A12: x0 in left_closed_halfline x0 by LIMFUNC1:def 1;
then A13: ((f1 | I) | (left_closed_halfline x0)) . x0 = (f1 | I) . x0 by FUNCT_1:49;

per cases ( (f1 | I) . x0 = inf J or (f1 | I) . x0 = sup J or ( (f1 | I) . x0 <> inf J & (f1 | I) . x0 <> sup J ) ) ;

suppose A14: (f1 | I) . x0 = inf J ; :: thesis: ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A15: f2 | J is_right_differentiable_in (f1 | I) . x0 by A11, A2, Th11;
then A16: f2 is_right_differentiable_in f1 . x0 by A9, Th9;
consider R2 being Real such that
A17: ( R2 > 0 & [.((f1 | I) . x0),(((f1 | I) . x0) + R2).] c= dom (f2 | J) ) by A15, FDIFF_3:def 3;
set F2 = (f2 | J) | (right_closed_halfline ((f1 | I) . x0));
f1 | I is_Lcontinuous_in x0 by A7, A6, FDIFF_3:5;
then A18: for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom ((f1 | I) | (left_closed_halfline x0)) & |.(x - x0).| < d holds
|.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < e ) ) by Th36, FCONT_1:3;
A19: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )

proof

let r1 be Real; :: thesis: ( r1 > 0 implies ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) )
set s = min ((r1 / 2),R2);
assume A20: r1 > 0 ; :: thesis: ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
A21: ( 0 < r1 / 2 & r1 / 2 < r1 ) by A20, XREAL_1:215, XREAL_1:216;
then A22: ( 0 < min ((r1 / 2),R2) & min ((r1 / 2),R2) <= r1 / 2 & min ((r1 / 2),R2) <= R2 ) by A17, XXREAL_0:17, XXREAL_0:21;
consider d2 being Real such that
A23: ( 0 < d2 & ( for x being Real st x in dom ((f1 | I) | (left_closed_halfline x0)) & |.(x - x0).| < d2 holds
|.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < min ((r1 / 2),R2) ) ) by A18, A21, A17, XXREAL_0:21;
set r0 = min ((d2 / 2),R1);
A24: ( 0 < d2 / 2 & d2 / 2 < d2 ) by A23, XREAL_1:215, XREAL_1:216;
then A25: ( 0 < min ((d2 / 2),R1) & min ((d2 / 2),R1) <= d2 / 2 & min ((d2 / 2),R1) <= R1 ) by A8, XXREAL_0:17, XXREAL_0:21;
x0 - R1 <= x0 - (min ((d2 / 2),R1)) by XXREAL_0:17, XREAL_1:10;
then A26: [.(x0 - (min ((d2 / 2),R1))),x0.] c= [.(x0 - R1),x0.] by XXREAL_1:34;
take min ((d2 / 2),R1) ; :: thesis: ( min ((d2 / 2),R1) > 0 & [.(x0 - (min ((d2 / 2),R1))),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
thus min ((d2 / 2),R1) > 0 by A8, A24, XXREAL_0:21; :: thesis: [.(x0 - (min ((d2 / 2),R1))),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)

now :: thesis: for x being Real st x in [.(x0 - (min ((d2 / 2),R1))),x0.] holds
x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)

let x be Real; :: thesis: ( x in [.(x0 - (min ((d2 / 2),R1))),x0.] implies x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
assume A27: x in [.(x0 - (min ((d2 / 2),R1))),x0.] ; :: thesis: x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)
then A28: x in dom (f1 | I) by A26, A8;
then A29: ( x in dom f1 & x in I ) by RELAT_1:57;
then A30: f1 . x in f1 .: I by FUNCT_1:def 6;
( J = [.(inf J),(sup J).[ or J = [.(inf J),(sup J).] ) by A11, A14, Lm23;
then A31: (f1 | I) . x0 <= f1 . x by A3, A14, A30, XXREAL_1:1, XXREAL_1:3;
A32: ( x0 - (min ((d2 / 2),R1)) <= x & x <= x0 ) by A27, XXREAL_1:1;
then |.(x - x0).| = - (x - x0) by ABSVALUE:30, XREAL_1:47;
then |.(x - x0).| <= - (- (min ((d2 / 2),R1))) by A32, XREAL_1:19, XREAL_1:24;
then |.(x - x0).| <= d2 / 2 by A25, XXREAL_0:2;
then A33: |.(x - x0).| < d2 by A24, XXREAL_0:2;
x in ].-infty,x0.] by A32, XXREAL_1:234;
then A34: x in left_closed_halfline x0 by LIMFUNC1:def 1;
then |.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < min ((r1 / 2),R2) by A23, A33, A28, RELAT_1:57;
then |.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < r1 / 2 by A22, XXREAL_0:2;
then A35: |.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < r1 by A21, XXREAL_0:2;
x in dom ((f1 | I) | (left_closed_halfline x0)) by A28, A34, RELAT_1:57;
then A36: ( ((f1 | I) | (left_closed_halfline x0)) . x = (f1 | I) . x & (f1 | I) . x = f1 . x ) by A26, A8, A27, FUNCT_1:47;
then ((f1 | I) | (left_closed_halfline x0)) . x0 <= ((f1 | I) | (left_closed_halfline x0)) . x by A31, A12, FUNCT_1:49;
then |.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| = (((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0) by XREAL_1:48, ABSVALUE:def 1;
then ((f1 | I) | (left_closed_halfline x0)) . x < (((f1 | I) | (left_closed_halfline x0)) . x0) + r1 by A35, XREAL_1:19;
hence x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) by A29, A9, A13, A31, A36, FUNCT_1:54, XXREAL_1:1; :: thesis: verum

end;

hence [.(x0 - (min ((d2 / 2),R1))),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ; :: thesis: verum

end;

hence f2 * f1 is_left_differentiable_in x0 by A6, A4, A5, A1, A16, Th43; :: thesis: Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A6, A4, A5, A1, A16, A19, Th43
.= (Rdiff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A4, A5, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A9, A2, A3, A10, A14, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

suppose A37: (f1 | I) . x0 = sup J ; :: thesis: ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A38: f2 | J is_left_differentiable_in (f1 | I) . x0 by A11, A2, Th11;
A39: f2 is_left_differentiable_in f1 . x0 by A38, A9, Th10;
consider R2 being Real such that
A40: ( R2 > 0 & [.(((f1 | I) . x0) - R2),((f1 | I) . x0).] c= dom (f2 | J) ) by A38, FDIFF_3:def 4;
set F2 = (f2 | J) | (left_closed_halfline ((f1 | I) . x0));
f1 | I is_Lcontinuous_in x0 by A6, A7, FDIFF_3:5;
then A41: for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom ((f1 | I) | (left_closed_halfline x0)) & |.(x - x0).| < d holds
|.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < e ) ) by Th36, FCONT_1:3;
A42: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )

proof

let r1 be Real; :: thesis: ( r1 > 0 implies ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) ) )
set s = min ((r1 / 2),R2);
assume r1 > 0 ; :: thesis: ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
then A44: ( 0 < r1 / 2 & r1 / 2 < r1 ) by XREAL_1:215, XREAL_1:216;
then A45: ( 0 < min ((r1 / 2),R2) & min ((r1 / 2),R2) <= r1 / 2 & min ((r1 / 2),R2) <= R2 ) by A40, XXREAL_0:17, XXREAL_0:21;
consider d2 being Real such that
A46: ( 0 < d2 & ( for x being Real st x in dom ((f1 | I) | (left_closed_halfline x0)) & |.(x - x0).| < d2 holds
|.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < min ((r1 / 2),R2) ) ) by A41, A44, A40, XXREAL_0:21;
set r0 = min ((d2 / 2),R1);
A47: ( 0 < d2 / 2 & d2 / 2 < d2 ) by A46, XREAL_1:215, XREAL_1:216;
then A48: ( 0 < min ((d2 / 2),R1) & min ((d2 / 2),R1) <= d2 / 2 & min ((d2 / 2),R1) <= R1 ) by A8, XXREAL_0:17, XXREAL_0:21;
x0 - R1 <= x0 - (min ((d2 / 2),R1)) by XXREAL_0:17, XREAL_1:10;
then A49: [.(x0 - (min ((d2 / 2),R1))),x0.] c= [.(x0 - R1),x0.] by XXREAL_1:34;
take min ((d2 / 2),R1) ; :: thesis: ( min ((d2 / 2),R1) > 0 & [.(x0 - (min ((d2 / 2),R1))),x0.] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
thus min ((d2 / 2),R1) > 0 by A8, A47, XXREAL_0:21; :: thesis: [.(x0 - (min ((d2 / 2),R1))),x0.] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1)

now :: thesis: for x being Real st x in [.(x0 - (min ((d2 / 2),R1))),x0.] holds
x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1)

let x be Real; :: thesis: ( x in [.(x0 - (min ((d2 / 2),R1))),x0.] implies x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
assume A50: x in [.(x0 - (min ((d2 / 2),R1))),x0.] ; :: thesis: x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1)
then A51: x in dom (f1 | I) by A8, A49;
then A52: ( x in dom f1 & x in I ) by RELAT_1:57;
then A53: f1 . x in f1 .: I by FUNCT_1:def 6;
( J = [.(inf J),(sup J).] or J = ].(inf J),(sup J).] ) by A11, A37, Lm24;
then A54: f1 . x <= (f1 | I) . x0 by A3, A37, A53, XXREAL_1:1, XXREAL_1:2;
A55: ( x0 - (min ((d2 / 2),R1)) <= x & x <= x0 ) by A50, XXREAL_1:1;
then |.(x - x0).| = - (x - x0) by ABSVALUE:30, XREAL_1:47;
then |.(x - x0).| <= - (- (min ((d2 / 2),R1))) by A55, XREAL_1:19, XREAL_1:24;
then |.(x - x0).| <= d2 / 2 by A48, XXREAL_0:2;
then A56: |.(x - x0).| < d2 by A47, XXREAL_0:2;
x in ].-infty,x0.] by A55, XXREAL_1:234;
then A57: x in left_closed_halfline x0 by LIMFUNC1:def 1;
then |.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < min ((r1 / 2),R2) by A46, A56, A51, RELAT_1:57;
then A58: |.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| < r1 / 2 by A45, XXREAL_0:2;
x in dom ((f1 | I) | (left_closed_halfline x0)) by A51, A57, RELAT_1:57;
then A59: ( ((f1 | I) | (left_closed_halfline x0)) . x = (f1 | I) . x & (f1 | I) . x = f1 . x ) by A50, A8, A49, FUNCT_1:47;
then ((f1 | I) | (left_closed_halfline x0)) . x0 >= ((f1 | I) | (left_closed_halfline x0)) . x by A54, A12, FUNCT_1:49;
then |.((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)).| = - ((((f1 | I) | (left_closed_halfline x0)) . x) - (((f1 | I) | (left_closed_halfline x0)) . x0)) by ABSVALUE:30, XREAL_1:47;
then (((f1 | I) | (left_closed_halfline x0)) . x0) - (((f1 | I) | (left_closed_halfline x0)) . x) < r1 by A58, A44, XXREAL_0:2;
then ((f1 | I) | (left_closed_halfline x0)) . x0 < (((f1 | I) | (left_closed_halfline x0)) . x) + r1 by XREAL_1:19;
then (((f1 | I) | (left_closed_halfline x0)) . x0) - r1 < ((f1 | I) | (left_closed_halfline x0)) . x by XREAL_1:19;
hence x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) by A52, A9, A13, A54, A59, FUNCT_1:54, XXREAL_1:1; :: thesis: verum

end;

hence [.(x0 - (min ((d2 / 2),R1))),x0.] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) ; :: thesis: verum

end;

hence f2 * f1 is_left_differentiable_in x0 by A6, A4, A5, A1, A39, Th46; :: thesis: Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
Ldiff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A6, A4, A5, A1, A39, A42, Th46
.= (Ldiff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A4, A5, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A9, A2, A3, A10, A37, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

suppose A60: ( (f1 | I) . x0 <> inf J & (f1 | I) . x0 <> sup J ) ; :: thesis: ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then (f1 | I) . x0 in ].(inf J),(sup J).[ by A11, Th3;
then A61: f2 is_differentiable_in (f1 | I) . x0 by A11, A2, Th11;
hence f2 * f1 is_left_differentiable_in x0 by A6, A4, A5, A9, A1, Th41; :: thesis: Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
Ldiff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A61, A9, A6, A4, A5, A1, Th41
.= (diff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A4, A5, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A2, A3, A10, A60, A9, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

end;