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

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

let x be Real; :: thesis: ( x in [.x0,(x0 + r).] implies x in dom (f2 * f1) )
assume A15: x in [.x0,(x0 + r).] ; :: thesis: x in dom (f2 * f1)
x0 <= x by A15, XXREAL_1:1;
then x in [.x0,+infty.[ by XXREAL_1:236;
then A16: x in right_closed_halfline x0 by LIMFUNC1:def 2;
then A17: (f1 | (right_closed_halfline x0)) . x = f1 . x by FUNCT_1:49;
A18: x in dom (f1 | (right_closed_halfline x0)) by A15, A14, A16, RELAT_1:57;
(f1 | (right_closed_halfline x0)) . x in (f1 | (right_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,(x0 + r).] c= dom (f2 * f1) ; :: thesis: verum