let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom (f2 * f1) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_left_differentiable_in x0 & f2 is_differentiable_in f1 . x0 implies ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom (f2 * f1) ) )
assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_differentiable_in f1 . x0 ; :: thesis: ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom (f2 * f1) )
consider r1 being Real such that
A3: ( r1 > 0 & [.(x0 - r1),x0.] c= dom f1 ) by A1, FDIFF_3:def 4;
consider N2 being Neighbourhood of f1 . x0 such that
A4: N2 c= dom f2 by A2;
x0 in ].-infty,x0.] by XXREAL_1:234;
then A5: x0 in left_closed_halfline x0 by LIMFUNC1:def 1;
set ff1 = f1 | (left_closed_halfline x0);
reconsider N2 = N2 as Neighbourhood of (f1 | (left_closed_halfline x0)) . x0 by A5, FUNCT_1:49;
f1 | (left_closed_halfline x0) is_continuous_in x0 by A1, FDIFF_3:5, Th36;
then consider N3 being Neighbourhood of x0 such that
A6: (f1 | (left_closed_halfline x0)) .: N3 c= N2 by FCONT_1:5;
consider r2 being Real such that
A7: ( r2 > 0 & N3 = ].(x0 - r2),(x0 + r2).[ ) by RCOMP_1:def 6;
set r3 = min (r1,r2);
A8: min (r1,r2) > 0 by A3, A7, XXREAL_0:21;
A9: ( x0 - r1 <= x0 - (min (r1,r2)) & x0 - r2 <= x0 - (min (r1,r2)) ) by XREAL_1:10, XXREAL_0:17;
consider x1 being Real such that
A10: ( x0 - (min (r1,r2)) < x1 & x1 < x0 ) by A8, XREAL_1:5, XREAL_1:44;
take r = x0 - x1; :: thesis: ( r > 0 & [.(x0 - r),x0.] c= dom (f2 * f1) )
thus r > 0 by A10, XREAL_1:50; :: thesis: [.(x0 - r),x0.] c= dom (f2 * f1)
A11: x0 < x0 + r2 by A7, XREAL_1:29;
A12: ( x0 - r1 < x0 - r & x0 - r2 < x0 - r ) by A9, A10, XXREAL_0:2;
then A13: [.(x0 - r),x0.] c= N3 by A7, A11, XXREAL_1:47;
[.(x0 - r),x0.] c= [.(x0 - r1),x0.] by A12, XXREAL_1:34;
then A14: [.(x0 - r),x0.] c= dom f1 by A3;

now :: thesis: for x being Real st x in [.(x0 - r),x0.] holds
x in dom (f2 * f1)

let x be Real; :: thesis: ( x in [.(x0 - r),x0.] implies x in dom (f2 * f1) )
assume A15: x in [.(x0 - r),x0.] ; :: thesis: x in dom (f2 * f1)
x <= x0 by A15, XXREAL_1:1;
then x in ].-infty,x0.] by XXREAL_1:234;
then A16: x in left_closed_halfline x0 by LIMFUNC1:def 1;
then A17: (f1 | (left_closed_halfline x0)) . x = f1 . x by FUNCT_1:49;
A18: x in dom (f1 | (left_closed_halfline x0)) by A15, A14, A16, RELAT_1:57;
(f1 | (left_closed_halfline x0)) . x in (f1 | (left_closed_halfline x0)) .: N3 by A13, A15, A18, FUNCT_1:def 6;
then f1 . x in dom f2 by A6, A4, A17;
hence x in dom (f2 * f1) by A15, A14, FUNCT_1:11; :: thesis: verum

end;

hence [.(x0 - r),x0.] c= dom (f2 * f1) ; :: thesis: verum