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

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

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

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

then A17: ( x0 < x & x < x0 + d ) by A14, A16, XXREAL_0:1, XXREAL_0:2;
then A18: |.((f1 . x) - (f1 . x0)).| < r1 by A8, A15;
x0 + r0 <= x0 + R by XXREAL_0:17, XREAL_1:6;
then A19: ( x0 < x0 + R & x <= x0 + R ) by A4, A14, XREAL_1:29, XXREAL_0:2;
then ( x0 in dom (f1 | [.x0,(x0 + R).]) & x in dom (f1 | [.x0,(x0 + R).]) ) by A6, A15, A14, XXREAL_1:1, RELAT_1:57;
then (f1 | [.x0,(x0 + R).]) . x0 >= (f1 | [.x0,(x0 + R).]) . x by A4, A17, RFUNCT_2:def 4;
then f1 . x0 >= (f1 | [.x0,(x0 + R).]) . 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, XREAL_1:47, ABSVALUE:30;
then (f1 . x0) - (f1 . x) < r1 ;
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 A15, A20, XXREAL_1:1, FUNCT_1:54; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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