let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ex r being Real st
( r > 0 & f1 | [.(x0 - r),x0.] is non-increasing ) holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_left_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ex r being Real st
( r > 0 & f1 | [.(x0 - r),x0.] is non-increasing ) implies ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) )
assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_right_differentiable_in f1 . x0 and
A3: ex r being Real st
( r > 0 & f1 | [.(x0 - r),x0.] is non-increasing ) ; :: thesis: ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
consider R being Real such that
A4: ( R > 0 & f1 | [.(x0 - R),x0.] is non-increasing ) by A3;
A5: f1 is_Lcontinuous_in x0 by A1, FDIFF_3:5;
then A6: x0 in dom f1 by Th27;
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) ) )
assume A7: r1 > 0 ; :: thesis: ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
then consider d being Real such that
A8: ( 0 < d & ( for x being Real st x in dom f1 & x0 - d < x & x < x0 holds
|.((f1 . x) - (f1 . x0)).| < r1 ) ) by A5, Th27;
A9: ( 0 < d / 2 & d / 2 < d ) by A8, XREAL_1:215, XREAL_1:216;
consider s0 being Real such that
A10: ( s0 > 0 & [.(x0 - s0),x0.] c= dom f1 ) by A1, FDIFF_3:def 4;
set e = min ((d / 2),s0);
take r0 = min ((min ((d / 2),s0)),R); :: thesis: ( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
A11: min ((d / 2),s0) > 0 by A9, A10, XXREAL_0:21;
( min ((d / 2),s0) <= d / 2 & min ((d / 2),s0) <= s0 & r0 <= min ((d / 2),s0) & r0 <= R ) by XXREAL_0:17;
then A12: ( r0 <= d / 2 & r0 <= s0 & r0 <= R ) by XXREAL_0:2;
then A13: r0 < d by A9, XXREAL_0:2;

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

let x be Real; :: thesis: ( x in [.(x0 - r0),x0.] implies b₁ in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) )
assume x in [.(x0 - r0),x0.] ; :: thesis: b<sub>1</sub> in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)
then A14: ( x0 - r0 <= x & x <= x0 ) by XXREAL_1:1;
x0 - s0 <= x0 - r0 by A12, XREAL_1:10;
then x0 - s0 <= x by A14, XXREAL_0:2;
then A15: x in dom f1 by A10, A14, XXREAL_1:1;
A16: x0 - d < x0 - r0 by A13, XREAL_1:15;

per cases ( x <> x0 or x = x0 ) ;

suppose x <> x0 ; :: thesis: b₁ in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)

then A17: ( x0 - d < x & x < x0 ) by A14, A16, XXREAL_0:1, XXREAL_0:2;
then A18: |.((f1 . x) - (f1 . x0)).| < r1 by A8, A15;
x0 - R <= x0 - r0 by XXREAL_0:17, XREAL_1:10;
then A19: ( x0 - R < x0 & x0 - R <= x ) by A4, A14, XREAL_1:44, XXREAL_0:2;
then ( x0 in dom (f1 | [.(x0 - R),x0.]) & x in dom (f1 | [.(x0 - R),x0.]) ) by A6, A15, A14, XXREAL_1:1, RELAT_1:57;
then (f1 | [.(x0 - R),x0.]) . x0 <= (f1 | [.(x0 - R),x0.]) . x by A4, A17, RFUNCT_2:def 4;
then f1 . x0 <= (f1 | [.(x0 - R),x0.]) . x by A19, XXREAL_1:1, FUNCT_1:49;
then A20: f1 . x0 <= f1 . x by A19, A14, XXREAL_1:1, FUNCT_1:49;
then (f1 . x) - (f1 . x0) < r1 by A18, ABSVALUE:def 1, XREAL_1:48;
then f1 . x < (f1 . x0) + r1 by XREAL_1:19;
hence x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) by A15, A20, XXREAL_1:1, FUNCT_1:54; :: thesis: verum

end;

suppose x = x0 ; :: thesis: b₁ in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1)

then ( f1 . x0 <= f1 . x & f1 . x < (f1 . x0) + r1 ) by A7, XREAL_1:29;
hence x in dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) by A15, FUNCT_1:54, XXREAL_1:1; :: thesis: verum

end;

end;

end;

hence ( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) by A11, A4, XXREAL_0:21; :: thesis: verum

end;

hence ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) by A1, A2, Th43; :: thesis: verum