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 holds
( f2 * f1 is_differentiable_on_interval I & (f2 * f1) `\ I = ((f2 `\ J) * f1) (#) (f1 `\ I) )
let I, J be non empty Interval; :: thesis: ( f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J implies ( f2 * f1 is_differentiable_on_interval I & (f2 * f1) `\ I = ((f2 `\ J) * f1) (#) (f1 `\ I) ) )
assume that
A1: f1 is_differentiable_on_interval I and
A2: f2 is_differentiable_on_interval J and
A3: f1 .: I c= J ; :: thesis: ( f2 * f1 is_differentiable_on_interval I & (f2 * f1) `\ I = ((f2 `\ J) * f1) (#) (f1 `\ I) )
J c= dom f2 by A2;
then f1 .: I c= dom f2 by A3;
then A4: I c= dom (f2 * f1) by A1, FUNCT_1:101;
for x being Real st x in I holds
( ( x = inf I implies (f2 * f1) | I is_right_differentiable_in x ) & ( x = sup I implies (f2 * f1) | I is_left_differentiable_in x ) & ( x in ].(inf I),(sup I).[ implies f2 * f1 is_differentiable_in x ) ) by A1, A2, A3, Th4, Lm26, Th5, Lm27, Lm28;
hence A5: f2 * f1 is_differentiable_on_interval I by A4, Th11; :: thesis: (f2 * f1) `\ I = ((f2 `\ J) * f1) (#) (f1 `\ I)
A6: ( dom (f1 `\ I) = I & dom (f2 `\ J) = J ) by A1, A2, Def2;
then f1 " J = dom ((f2 `\ J) * f1) by RELAT_1:147;
then A7: f1 " (f1 .: I) c= dom ((f2 `\ J) * f1) by A3, RELAT_1:143;
I c= f1 " (f1 .: I) by A1, FUNCT_1:76;
then I c= dom ((f2 `\ J) * f1) by A7;
then (dom ((f2 `\ J) * f1)) /\ (dom (f1 `\ I)) = I by A6, XBOOLE_1:28;
then A8: dom (((f2 `\ J) * f1) (#) (f1 `\ I)) = I by VALUED_1:def 4;

now :: thesis: for x being Real st x in I holds
( ( x = inf I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Rdiff ((f2 * f1),x) ) & ( x = sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Ldiff ((f2 * f1),x) ) & ( x <> inf I & x <> sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = diff ((f2 * f1),x) ) )

let x be Real; :: thesis: ( x in I implies ( ( x = inf I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Rdiff ((f2 * f1),x) ) & ( x = sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Ldiff ((f2 * f1),x) ) & ( x <> inf I & x <> sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = diff ((f2 * f1),x) ) ) )
assume A9: x in I ; :: thesis: ( ( x = inf I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Rdiff ((f2 * f1),x) ) & ( x = sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Ldiff ((f2 * f1),x) ) & ( x <> inf I & x <> sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = diff ((f2 * f1),x) ) )
hence ( x = inf I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Rdiff ((f2 * f1),x) ) by A1, A2, A3, Lm26; :: thesis: ( ( x = sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Ldiff ((f2 * f1),x) ) & ( x <> inf I & x <> sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = diff ((f2 * f1),x) ) )
thus ( x = sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = Ldiff ((f2 * f1),x) ) by A1, A2, A3, A9, Lm27; :: thesis: ( x <> inf I & x <> sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = diff ((f2 * f1),x) )
thus ( x <> inf I & x <> sup I implies (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = diff ((f2 * f1),x) ) :: thesis: verum

proof

assume ( x <> inf I & x <> sup I ) ; :: thesis: (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = diff ((f2 * f1),x)
then x in ].(inf I),(sup I).[ by A9, Th3;
hence (((f2 `\ J) * f1) (#) (f1 `\ I)) . x = diff ((f2 * f1),x) by A1, A2, A3, A9, Lm28; :: thesis: verum

end;

end;

hence (f2 * f1) `\ I = ((f2 `\ J) * f1) (#) (f1 `\ I) by A5, A8, Def2; :: thesis: verum