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 = inf I & x0 in I holds
( f2 * f1 is_right_differentiable_in x0 & Rdiff ((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 = inf I & x0 in I holds
( f2 * f1 is_right_differentiable_in x0 & Rdiff ((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 = inf I & x0 in I implies ( f2 * f1 is_right_differentiable_in x0 & Rdiff ((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 = inf I and
A5: x0 in I ; :: thesis: ( f2 * f1 is_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )
A6: inf I = lower_bound I by A4, A5, Lm5;
then A7: f1 | I is_right_differentiable_in lower_bound I by A4, A5, A1, Th11;
A8: f1 . x0 = (f1 | I) . x0 by A5, FUNCT_1:49;
A9: f1 . x0 in f1 .: I by A5, A1, FUNCT_1:def 6;
then f1 . x0 in J by A3;
then A10: (f1 | I) . x0 in J by A5, FUNCT_1:49;
consider R1 being Real such that
A11: ( R1 > 0 & [.x0,(x0 + R1).] c= dom (f1 | I) ) by A7, A4, A6, FDIFF_3:def 3;
set F1 = (f1 | I) | (right_closed_halfline x0);
x0 in [.x0,+infty.[ by XXREAL_1:236;
then A12: x0 in right_closed_halfline x0 by LIMFUNC1:def 2;
then A13: ((f1 | I) | (right_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_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A15: f2 | J is_right_differentiable_in (f1 | I) . x0 by A10, A2, Th11;
then A16: f2 is_right_differentiable_in f1 . x0 by A8, 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_Rcontinuous_in x0 by A7, A4, A6, FDIFF_3:7;
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) | (right_closed_halfline x0)) & |.(x - x0).| < d holds
|.((((f1 | I) | (right_closed_halfline x0)) . x) - (((f1 | I) | (right_closed_halfline x0)) . x0)).| < e ) ) by Th35, FCONT_1:3;
A19: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.x0,(x0 + r0).] 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,(x0 + r0).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) )
set s = min ((r1 / 2),R2);
assume r1 > 0 ; :: thesis: ex r0 being Real st
( r0 > 0 & [.x0,(x0 + r0).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
then A20: ( 0 < r1 / 2 & r1 / 2 < r1 ) by XREAL_1:215, XREAL_1:216;
then consider d2 being Real such that
A21: ( 0 < d2 & ( for x being Real st x in dom ((f1 | I) | (right_closed_halfline x0)) & |.(x - x0).| < d2 holds
|.((((f1 | I) | (right_closed_halfline x0)) . x) - (((f1 | I) | (right_closed_halfline x0)) . x0)).| < min ((r1 / 2),R2) ) ) by A18, A17, XXREAL_0:21;
set r0 = min ((d2 / 2),R1);
A22: ( 0 < min ((r1 / 2),R2) & min ((r1 / 2),R2) <= r1 / 2 & min ((r1 / 2),R2) <= R2 ) by A20, A17, XXREAL_0:17, XXREAL_0:21;
A23: ( 0 < d2 / 2 & d2 / 2 < d2 ) by A21, XREAL_1:215, XREAL_1:216;
then A24: ( 0 < min ((d2 / 2),R1) & min ((d2 / 2),R1) <= d2 / 2 & min ((d2 / 2),R1) <= R1 ) by A11, XXREAL_0:17, XXREAL_0:21;
x0 + (min ((d2 / 2),R1)) <= x0 + R1 by XXREAL_0:17, XREAL_1:6;
then A25: [.x0,(x0 + (min ((d2 / 2),R1))).] c= [.x0,(x0 + R1).] by XXREAL_1:34;
take min ((d2 / 2),R1) ; :: thesis: ( min ((d2 / 2),R1) > 0 & [.x0,(x0 + (min ((d2 / 2),R1))).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
thus min ((d2 / 2),R1) > 0 by A11, A23, XXREAL_0:21; :: thesis: [.x0,(x0 + (min ((d2 / 2),R1))).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)

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

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

end;

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

end;

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

end;

suppose A36: (f1 | I) . x0 = sup J ; :: thesis: ( f2 * f1 is_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A37: f2 | J is_left_differentiable_in (f1 | I) . x0 by A10, A2, Th11;
then A38: f2 is_left_differentiable_in f1 . x0 by A8, Th10;
consider R2 being Real such that
A39: ( R2 > 0 & [.(((f1 | I) . x0) - R2),((f1 | I) . x0).] c= dom (f2 | J) ) by A37, FDIFF_3:def 4;
set F2 = (f2 | J) | (left_closed_halfline ((f1 | I) . x0));
A40: (f1 | I) | (right_closed_halfline x0) is_continuous_in x0 by A4, A6, A7, FDIFF_3:7, Th35;
A41: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.x0,(x0 + r0).] 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,(x0 + r0).] 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,(x0 + r0).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
then A42: ( 0 < r1 / 2 & r1 / 2 < r1 ) by XREAL_1:215, XREAL_1:216;
then A43: ( 0 < min ((r1 / 2),R2) & min ((r1 / 2),R2) <= r1 / 2 & min ((r1 / 2),R2) <= R2 ) by A39, XXREAL_0:17, XXREAL_0:21;
consider d2 being Real such that
A44: ( 0 < d2 & ( for x being Real st x in dom ((f1 | I) | (right_closed_halfline x0)) & |.(x - x0).| < d2 holds
|.((((f1 | I) | (right_closed_halfline x0)) . x) - (((f1 | I) | (right_closed_halfline x0)) . x0)).| < min ((r1 / 2),R2) ) ) by A40, A42, A39, XXREAL_0:21, FCONT_1:3;
set r0 = min ((d2 / 2),R1);
A45: ( 0 < d2 / 2 & d2 / 2 < d2 ) by A44, XREAL_1:215, XREAL_1:216;
then A46: ( 0 < min ((d2 / 2),R1) & min ((d2 / 2),R1) <= d2 / 2 & min ((d2 / 2),R1) <= R1 ) by A11, XXREAL_0:17, XXREAL_0:21;
x0 + (min ((d2 / 2),R1)) <= x0 + R1 by XXREAL_0:17, XREAL_1:6;
then A47: [.x0,(x0 + (min ((d2 / 2),R1))).] c= [.x0,(x0 + R1).] by XXREAL_1:34;
take min ((d2 / 2),R1) ; :: thesis: ( min ((d2 / 2),R1) > 0 & [.x0,(x0 + (min ((d2 / 2),R1))).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
thus min ((d2 / 2),R1) > 0 by A11, A45, XXREAL_0:21; :: thesis: [.x0,(x0 + (min ((d2 / 2),R1))).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1)

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

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

end;

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

end;

hence f2 * f1 is_right_differentiable_in x0 by A4, A6, A5, A1, A38, Th45; :: thesis: Rdiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
Rdiff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (Rdiff (f1,x0)) by A4, A6, A5, A1, A38, A41, Th45
.= (Ldiff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A4, A5, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A8, A2, A3, A9, A36, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence Rdiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

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

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

end;

end;