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 in ].(inf I),(sup I).[ & x0 in I holds
( f2 * f1 is_differentiable_in x0 & diff ((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 in ].(inf I),(sup I).[ & x0 in I holds
( f2 * f1 is_differentiable_in x0 & diff ((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 in ].(inf I),(sup I).[ & x0 in I implies ( f2 * f1 is_differentiable_in x0 & diff ((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 in ].(inf I),(sup I).[ and
A5: x0 in I ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )
A6: ( inf I < x0 & x0 < sup I ) by A4, XXREAL_1:4;
reconsider A = ].(inf I),(sup I).[ as open Subset of REAL by Th2;
A7: f1 is_differentiable_on A by A1;
A8: f1 . x0 in f1 .: I by A1, A5, FUNCT_1:def 6;
A9: f1 | A is_differentiable_in x0 by A4, A7;
then A10: f1 is_differentiable_in x0 by A4, PDIFFEQ1:2;
then A11: f1 is_continuous_in x0 by FDIFF_1:24;
consider R1 being Real such that
A12: ( 0 < R1 & ].(x0 - R1),(x0 + R1).[ c= A ) by A4, RCOMP_1:19;
A13: ( 0 < R1 / 2 & R1 / 2 < R1 ) by A12, XREAL_1:215, XREAL_1:216;
A14: A c= I by Th2;
then x0 in I by A4;
then f1 . x0 in f1 .: I by A1, FUNCT_1:def 6;
then A15: f1 . x0 in J by A3;

per cases ( ( inf J in J & sup J in J ) or ( not inf J in J & sup J in J ) or ( inf J in J & not sup J in J ) or ( not inf J in J & not sup J in J ) ) ;

suppose A16: ( inf J in J & sup J in J ) ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

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

suppose A17: f1 . x0 = inf J ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A18: f2 is_right_differentiable_in f1 . x0 by A2, A16, Lm5;
then consider R2 being Real such that
A19: ( R2 > 0 & [.(f1 . x0),((f1 . x0) + R2).] c= dom f2 ) by FDIFF_3:def 3;
A20: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),(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 - r0),(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 - r0),(x0 + r0).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
then A21: ( 0 < r1 / 2 & r1 / 2 < r1 ) by 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 A19, XXREAL_0:17, XXREAL_0:21;
consider d2 being Real such that
A23: ( 0 < d2 & ( for x being Real st x in dom f1 & |.(x - x0).| < d2 holds
|.((f1 . x) - (f1 . x0)).| < min ((r1 / 2),R2) ) ) by A11, A21, A19, XXREAL_0:21, FCONT_1:3;
set r0 = min ((d2 / 2),(R1 / 2));
A24: ( 0 < d2 / 2 & d2 / 2 < d2 ) by A23, XREAL_1:215, XREAL_1:216;
then A25: ( 0 < min ((d2 / 2),(R1 / 2)) & min ((d2 / 2),(R1 / 2)) <= d2 / 2 & min ((d2 / 2),(R1 / 2)) <= R1 / 2 ) by A13, XXREAL_0:17, XXREAL_0:21;
then min ((d2 / 2),(R1 / 2)) < R1 by A13, XXREAL_0:2;
then ( x0 - R1 < x0 - (min ((d2 / 2),(R1 / 2))) & x0 + (min ((d2 / 2),(R1 / 2))) < x0 + R1 ) by XREAL_1:8, XREAL_1:15;
then A26: [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= ].(x0 - R1),(x0 + R1).[ by XXREAL_1:47;
take min ((d2 / 2),(R1 / 2)) ; :: thesis: ( min ((d2 / 2),(R1 / 2)) > 0 & [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
thus min ((d2 / 2),(R1 / 2)) > 0 by A13, A24, XXREAL_0:21; :: thesis: [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)

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

let x be Real; :: thesis: ( x in [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] implies x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
assume A27: x in [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] ; :: thesis: x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)
then A28: x in I by A26, A12, A14;
then A29: f1 . x in f1 .: I by A1, FUNCT_1:def 6;
then A30: f1 . x0 <= f1 . x by A3, A17, XXREAL_2:3;
A31: (f1 . x) - (f1 . x0) >= 0 by A3, A29, A17, XXREAL_2:3, XREAL_1:48;
( x0 - (min ((d2 / 2),(R1 / 2))) <= x & x <= x0 + (min ((d2 / 2),(R1 / 2))) ) by A27, XXREAL_1:1;
then ( - (min ((d2 / 2),(R1 / 2))) <= x - x0 & x - x0 <= min ((d2 / 2),(R1 / 2)) ) by XREAL_1:19, XREAL_1:20;
then |.(x - x0).| <= min ((d2 / 2),(R1 / 2)) by ABSVALUE:5;
then |.(x - x0).| <= d2 / 2 by A25, XXREAL_0:2;
then |.(x - x0).| < d2 by A24, XXREAL_0:2;
then |.((f1 . x) - (f1 . x0)).| < min ((r1 / 2),R2) by A23, A28, A1;
then (f1 . x) - (f1 . x0) < min ((r1 / 2),R2) by A31, ABSVALUE:def 1;
then (f1 . x) - (f1 . x0) < r1 / 2 by A22, XXREAL_0:2;
then (f1 . x) - (f1 . x0) < r1 by A21, XXREAL_0:2;
then f1 . x < (f1 . x0) + r1 by XREAL_1:19;
hence x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) by A28, A30, A1, XXREAL_1:1, FUNCT_1:54; :: thesis: verum

end;

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

end;

hence f2 * f1 is_differentiable_in x0 by A10, A18, Th44; :: thesis: diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
diff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (diff (f1,x0)) by A20, A18, A10, Th44
.= (Rdiff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A5, A6, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A17, A8, A3, A2, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

suppose A32: f1 . x0 = sup J ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A33: f2 is_left_differentiable_in f1 . x0 by A2, A16, Lm6;
then consider R2 being Real such that
A34: ( R2 > 0 & [.((f1 . x0) - R2),(f1 . x0).] c= dom f2 ) by FDIFF_3:def 4;
A35: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),(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 - r0),(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 - r0),(x0 + r0).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
then A36: ( 0 < r1 / 2 & r1 / 2 < r1 ) by XREAL_1:215, XREAL_1:216;
then A37: ( 0 < min ((r1 / 2),R2) & min ((r1 / 2),R2) <= r1 / 2 & min ((r1 / 2),R2) <= R2 ) by A34, XXREAL_0:17, XXREAL_0:21;
consider d2 being Real such that
A38: ( 0 < d2 & ( for x being Real st x in dom f1 & |.(x - x0).| < d2 holds
|.((f1 . x) - (f1 . x0)).| < min ((r1 / 2),R2) ) ) by A11, A36, A34, XXREAL_0:21, FCONT_1:3;
set r0 = min ((d2 / 2),(R1 / 2));
A39: ( 0 < d2 / 2 & d2 / 2 < d2 ) by A38, XREAL_1:215, XREAL_1:216;
then A40: ( 0 < min ((d2 / 2),(R1 / 2)) & min ((d2 / 2),(R1 / 2)) <= d2 / 2 & min ((d2 / 2),(R1 / 2)) <= R1 / 2 ) by A13, XXREAL_0:17, XXREAL_0:21;
then min ((d2 / 2),(R1 / 2)) < R1 by A13, XXREAL_0:2;
then ( x0 - R1 < x0 - (min ((d2 / 2),(R1 / 2))) & x0 + (min ((d2 / 2),(R1 / 2))) < x0 + R1 ) by XREAL_1:8, XREAL_1:15;
then A41: [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= ].(x0 - R1),(x0 + R1).[ by XXREAL_1:47;
take min ((d2 / 2),(R1 / 2)) ; :: thesis: ( min ((d2 / 2),(R1 / 2)) > 0 & [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
thus min ((d2 / 2),(R1 / 2)) > 0 by A13, A39, XXREAL_0:21; :: thesis: [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1)

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

let x be Real; :: thesis: ( x in [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] implies x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
assume A42: x in [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] ; :: thesis: x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1)
then A43: x in I by A12, A14, A41;
then f1 . x in f1 .: I by A1, FUNCT_1:def 6;
then A44: f1 . x0 >= f1 . x by A3, A32, XXREAL_2:4;
( x0 - (min ((d2 / 2),(R1 / 2))) <= x & x <= x0 + (min ((d2 / 2),(R1 / 2))) ) by A42, XXREAL_1:1;
then ( - (min ((d2 / 2),(R1 / 2))) <= x - x0 & x - x0 <= min ((d2 / 2),(R1 / 2)) ) by XREAL_1:19, XREAL_1:20;
then |.(x - x0).| <= min ((d2 / 2),(R1 / 2)) by ABSVALUE:5;
then |.(x - x0).| <= d2 / 2 by A40, XXREAL_0:2;
then |.(x - x0).| < d2 by A39, XXREAL_0:2;
then |.((f1 . x) - (f1 . x0)).| < min ((r1 / 2),R2) by A38, A43, A1;
then - ((f1 . x) - (f1 . x0)) < min ((r1 / 2),R2) by A44, XREAL_1:47, ABSVALUE:30;
then (- (f1 . x)) + (f1 . x0) < r1 / 2 by A37, XXREAL_0:2;
then (f1 . x0) - (f1 . x) < r1 by A36, XXREAL_0:2;
then f1 . x0 < (f1 . x) + r1 by XREAL_1:19;
then (f1 . x0) - r1 < f1 . x by XREAL_1:19;
hence x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) by A1, A43, A44, XXREAL_1:1, FUNCT_1:54; :: thesis: verum

end;

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

end;

hence f2 * f1 is_differentiable_in x0 by A10, A33, Th47; :: thesis: diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
diff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (diff (f1,x0)) by A35, A33, A10, Th47
.= (Ldiff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A5, A6, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A32, A8, A3, A2, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

suppose A45: ( f1 . x0 <> inf J & f1 . x0 <> sup J ) ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then f1 . x0 in ].(inf J),(sup J).[ by A8, A3, Th3;
then A46: f2 is_differentiable_in f1 . x0 by A2, A8, A3, Th11;
hence f2 * f1 is_differentiable_in x0 by A10, FDIFF_2:13; :: thesis: diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A46, A10, FDIFF_2:13
.= (diff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A5, A6, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A45, A8, A3, A2, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

end;

end;

suppose A47: ( not inf J in J & sup J in J ) ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

per cases ( f1 . x0 = sup J or f1 . x0 <> sup J ) ;

suppose A48: f1 . x0 = sup J ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A49: f2 is_left_differentiable_in f1 . x0 by A2, A47, Lm6;
then consider R2 being Real such that
A50: ( R2 > 0 & [.((f1 . x0) - R2),(f1 . x0).] c= dom f2 ) by FDIFF_3:def 4;
A51: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),(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 - r0),(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 - r0),(x0 + r0).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
then A52: ( 0 < r1 / 2 & r1 / 2 < r1 ) by XREAL_1:215, XREAL_1:216;
then A53: ( 0 < min ((r1 / 2),R2) & min ((r1 / 2),R2) <= r1 / 2 & min ((r1 / 2),R2) <= R2 ) by A50, XXREAL_0:17, XXREAL_0:21;
consider d2 being Real such that
A54: ( 0 < d2 & ( for x being Real st x in dom f1 & |.(x - x0).| < d2 holds
|.((f1 . x) - (f1 . x0)).| < min ((r1 / 2),R2) ) ) by A11, A52, A50, XXREAL_0:21, FCONT_1:3;
set r0 = min ((d2 / 2),(R1 / 2));
A55: ( 0 < d2 / 2 & d2 / 2 < d2 ) by A54, XREAL_1:215, XREAL_1:216;
then A56: ( 0 < min ((d2 / 2),(R1 / 2)) & min ((d2 / 2),(R1 / 2)) <= d2 / 2 & min ((d2 / 2),(R1 / 2)) <= R1 / 2 ) by A13, XXREAL_0:17, XXREAL_0:21;
then min ((d2 / 2),(R1 / 2)) < R1 by A13, XXREAL_0:2;
then ( x0 - R1 < x0 - (min ((d2 / 2),(R1 / 2))) & x0 + (min ((d2 / 2),(R1 / 2))) < x0 + R1 ) by XREAL_1:8, XREAL_1:15;
then A57: [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= ].(x0 - R1),(x0 + R1).[ by XXREAL_1:47;
take min ((d2 / 2),(R1 / 2)) ; :: thesis: ( min ((d2 / 2),(R1 / 2)) > 0 & [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
thus min ((d2 / 2),(R1 / 2)) > 0 by A13, A55, XXREAL_0:21; :: thesis: [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1)

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

let x be Real; :: thesis: ( x in [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] implies x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) )
assume A58: x in [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] ; :: thesis: x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1)
then A59: x in I by A57, A14, A12;
then f1 . x in f1 .: I by A1, FUNCT_1:def 6;
then A60: f1 . x0 >= f1 . x by A3, A48, XXREAL_2:4;
( x0 - (min ((d2 / 2),(R1 / 2))) <= x & x <= x0 + (min ((d2 / 2),(R1 / 2))) ) by A58, XXREAL_1:1;
then ( - (min ((d2 / 2),(R1 / 2))) <= x - x0 & x - x0 <= min ((d2 / 2),(R1 / 2)) ) by XREAL_1:19, XREAL_1:20;
then |.(x - x0).| <= min ((d2 / 2),(R1 / 2)) by ABSVALUE:5;
then |.(x - x0).| <= d2 / 2 by A56, XXREAL_0:2;
then |.(x - x0).| < d2 by A55, XXREAL_0:2;
then |.((f1 . x) - (f1 . x0)).| < min ((r1 / 2),R2) by A1, A59, A54;
then - ((f1 . x) - (f1 . x0)) < min ((r1 / 2),R2) by A60, XREAL_1:47, ABSVALUE:30;
then (- (f1 . x)) + (f1 . x0) < r1 / 2 by A53, XXREAL_0:2;
then (f1 . x0) - (f1 . x) < r1 by A52, XXREAL_0:2;
then f1 . x0 < (f1 . x) + r1 by XREAL_1:19;
then (f1 . x0) - r1 < f1 . x by XREAL_1:19;
hence x in dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) by A1, A59, A60, XXREAL_1:1, FUNCT_1:54; :: thesis: verum

end;

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

end;

hence f2 * f1 is_differentiable_in x0 by A10, A49, Th47; :: thesis: diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
diff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (diff (f1,x0)) by A51, A49, A10, Th47
.= (Ldiff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A5, A6, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A48, A8, A3, A2, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

suppose A61: f1 . x0 <> sup J ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A62: f1 . x0 in ].(inf J),(sup J).[ by A47, A15, Th3;
then A63: f2 is_differentiable_in f1 . x0 by A2, A8, A3, Th11;
hence f2 * f1 is_differentiable_in x0 by A10, FDIFF_2:13; :: thesis: diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
A64: inf J < f1 . x0 by A62, XXREAL_1:4;
diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A63, A10, FDIFF_2:13
.= (diff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A5, A6, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A61, A8, A3, A64, A2, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

end;

end;

suppose A65: ( inf J in J & not sup J in J ) ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

per cases ( f1 . x0 = inf J or f1 . x0 <> inf J ) ;

suppose A66: f1 . x0 = inf J ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A67: f2 is_right_differentiable_in f1 . x0 by A2, A65, Lm5;
consider R2 being Real such that
A68: ( R2 > 0 & [.(f1 . x0),((f1 . x0) + R2).] c= dom f2 ) by A67, FDIFF_3:def 3;
A69: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),(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 - r0),(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 - r0),(x0 + r0).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
then A70: ( 0 < r1 / 2 & r1 / 2 < r1 ) by XREAL_1:215, XREAL_1:216;
then A71: ( 0 < min ((r1 / 2),R2) & min ((r1 / 2),R2) <= r1 / 2 & min ((r1 / 2),R2) <= R2 ) by A68, XXREAL_0:17, XXREAL_0:21;
then consider d2 being Real such that
A72: ( 0 < d2 & ( for x being Real st x in dom f1 & |.(x - x0).| < d2 holds
|.((f1 . x) - (f1 . x0)).| < min ((r1 / 2),R2) ) ) by A10, FDIFF_1:24, FCONT_1:3;
set r0 = min ((d2 / 2),(R1 / 2));
A73: ( 0 < d2 / 2 & d2 / 2 < d2 ) by A72, XREAL_1:215, XREAL_1:216;
then A74: ( 0 < min ((d2 / 2),(R1 / 2)) & min ((d2 / 2),(R1 / 2)) <= d2 / 2 & min ((d2 / 2),(R1 / 2)) <= R1 / 2 ) by A13, XXREAL_0:17, XXREAL_0:21;
then min ((d2 / 2),(R1 / 2)) < R1 by A13, XXREAL_0:2;
then ( x0 - R1 < x0 - (min ((d2 / 2),(R1 / 2))) & x0 + (min ((d2 / 2),(R1 / 2))) < x0 + R1 ) by XREAL_1:8, XREAL_1:15;
then A75: [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= ].(x0 - R1),(x0 + R1).[ by XXREAL_1:47;
take min ((d2 / 2),(R1 / 2)) ; :: thesis: ( min ((d2 / 2),(R1 / 2)) > 0 & [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
thus min ((d2 / 2),(R1 / 2)) > 0 by A13, A73, XXREAL_0:21; :: thesis: [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)

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

let x be Real; :: thesis: ( x in [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] implies x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
assume A76: x in [.(x0 - (min ((d2 / 2),(R1 / 2)))),(x0 + (min ((d2 / 2),(R1 / 2)))).] ; :: thesis: x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)
then A77: x in I by A75, A12, A14;
then f1 . x in f1 .: I by A1, FUNCT_1:def 6;
then A78: f1 . x0 <= f1 . x by A3, A66, XXREAL_2:3;
( x0 - (min ((d2 / 2),(R1 / 2))) <= x & x <= x0 + (min ((d2 / 2),(R1 / 2))) ) by A76, XXREAL_1:1;
then ( - (min ((d2 / 2),(R1 / 2))) <= x - x0 & x - x0 <= min ((d2 / 2),(R1 / 2)) ) by XREAL_1:19, XREAL_1:20;
then |.(x - x0).| <= min ((d2 / 2),(R1 / 2)) by ABSVALUE:5;
then |.(x - x0).| <= d2 / 2 by A74, XXREAL_0:2;
then |.(x - x0).| < d2 by A73, XXREAL_0:2;
then |.((f1 . x) - (f1 . x0)).| < min ((r1 / 2),R2) by A72, A1, A77;
then (f1 . x) - (f1 . x0) < min ((r1 / 2),R2) by A78, XREAL_1:48, ABSVALUE:def 1;
then (f1 . x) - (f1 . x0) < r1 / 2 by A71, XXREAL_0:2;
then (f1 . x) - (f1 . x0) < r1 by A70, XXREAL_0:2;
then f1 . x < (f1 . x0) + r1 by XREAL_1:19;
hence x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) by A1, A77, A78, XXREAL_1:1, FUNCT_1:54; :: thesis: verum

end;

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

end;

hence f2 * f1 is_differentiable_in x0 by A10, A67, Th44; :: thesis: diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
diff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (diff (f1,x0)) by A69, A67, A10, Th44
.= (Rdiff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A5, A6, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A66, A8, A3, A2, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

suppose A79: f1 . x0 <> inf J ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A80: f1 . x0 in ].(inf J),(sup J).[ by A65, A15, Th3;
then A81: f2 is_differentiable_in f1 . x0 by A2, A8, A3, Th11;
hence f2 * f1 is_differentiable_in x0 by A10, FDIFF_2:13; :: thesis: diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
A82: f1 . x0 < sup J by A80, XXREAL_1:4;
diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A81, A10, FDIFF_2:13
.= (diff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A5, A6, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A79, A8, A3, A82, A2, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

end;

end;

suppose A83: ( not inf J in J & not sup J in J ) ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

then A84: J = ].(inf J),(sup J).[ by Lm25;
reconsider B = ].(inf J),(sup J).[ as open Subset of REAL by Th2;
f2 is_differentiable_on B by A2;
then f2 | B is_differentiable_in f1 . x0 by A8, A3, A84;
then A85: ( f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 ) by A9, A8, A3, A84, A4, PDIFFEQ1:2;
A86: ( inf J < f1 . x0 & f1 . x0 < sup J ) by A84, A8, A3, XXREAL_1:4;
rng (f1 | A) = f1 .: A by RELAT_1:115;
then rng (f1 | A) c= f1 .: I by Th2, RELAT_1:123;
then rng (f1 | A) c= J by A3;
then rng (f1 | A) c= B by A83, Lm25;
then f2 * f1 is_differentiable_on A by A1, A2, Th1;
then (f2 * f1) | A is_differentiable_in x0 by A4;
hence f2 * f1 is_differentiable_in x0 by A4, PDIFFEQ1:2; :: thesis: diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0
diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A85, FDIFF_2:13
.= (diff (f2,(f1 . x0))) * ((f1 `\ I) . x0) by A5, A6, A1, Def2
.= ((f2 `\ J) . (f1 . x0)) * ((f1 `\ I) . x0) by A8, A3, A86, A2, Def2
.= (((f2 `\ J) * f1) . x0) * ((f1 `\ I) . x0) by A5, A1, FUNCT_1:13 ;
hence diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 by VALUED_1:5; :: thesis: verum

end;

end;