let f1, f2 be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 (#) f2 is_differentiable_on_interval I & (f1 (#) f2) `\ I = (f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I)) & ( for x being Real st x in I holds
((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) ) )
let I be non empty Interval; :: thesis: ( f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I implies ( f1 (#) f2 is_differentiable_on_interval I & (f1 (#) f2) `\ I = (f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I)) & ( for x being Real st x in I holds
((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) ) ) )
assume that
A1: f1 is_differentiable_on_interval I and
A2: f2 is_differentiable_on_interval I ; :: thesis: ( f1 (#) f2 is_differentiable_on_interval I & (f1 (#) f2) `\ I = (f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I)) & ( for x being Real st x in I holds
((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) ) )
reconsider J = ].(inf I),(sup I).[ as open Subset of REAL by Th2;
A3: J c= I by Th2;
A4: I c= (dom f1) /\ (dom f2) by A1, A2, XBOOLE_1:19;
then I c= dom (f1 (#) f2) by VALUED_1:def 4;
then J c= dom (f1 (#) f2) by A3;
hence A5: f1 (#) f2 is_differentiable_on_interval I by A4, A1, A2, FDIFF_1:21, FDIFF_3:18, FDIFF_3:12, VALUED_1:def 4; :: thesis: ( (f1 (#) f2) `\ I = (f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I)) & ( for x being Real st x in I holds
((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) ) )
then A6: dom ((f1 (#) f2) `\ I) = I by Def2;
A7: ( dom (f1 `\ I) = I & dom (f2 `\ I) = I ) by A1, A2, Def2;
( (dom f1) /\ (dom (f2 `\ I)) = I & (dom f2) /\ (dom (f1 `\ I)) = I ) by A1, A2, A7, XBOOLE_1:28;
then A8: ( dom (f1 (#) (f2 `\ I)) = I & dom (f2 (#) (f1 `\ I)) = I ) by VALUED_1:def 4;
then A9: dom ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) = I /\ I by VALUED_1:def 1;
A10: for x being Element of REAL st x in dom ((f1 (#) f2) `\ I) holds
((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((f1 (#) f2) `\ I) implies ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x )
assume x in dom ((f1 (#) f2) `\ I) ; :: thesis: ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x
then A11: x in I by A5, Def2;

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose A12: x = inf I ; :: thesis: ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x

then A13: ( ((f1 (#) f2) `\ I) . x = Rdiff ((f1 (#) f2),x) & (f1 `\ I) . x = Rdiff (f1,x) & (f2 `\ I) . x = Rdiff (f2,x) ) by A1, A2, A5, A11, Def2;
( f1 is_right_differentiable_in x & f2 is_right_differentiable_in x ) by A1, A2, A11, A12, Lm5;
then ((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) by A13, FDIFF_3:18;
then ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) . x) + ((f1 . x) * ((f2 `\ I) . x)) by A11, A8, VALUED_1:def 4;
then ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) . x) + ((f1 (#) (f2 `\ I)) . x) by A11, A8, VALUED_1:def 4;
hence ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x by A11, A9, VALUED_1:def 1; :: thesis: verum

end;

suppose A14: x = sup I ; :: thesis: ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x

then A15: ( ((f1 (#) f2) `\ I) . x = Ldiff ((f1 (#) f2),x) & (f1 `\ I) . x = Ldiff (f1,x) & (f2 `\ I) . x = Ldiff (f2,x) ) by A1, A2, A5, A11, Def2;
( f1 is_left_differentiable_in x & f2 is_left_differentiable_in x ) by A1, A2, A11, A14, Lm6;
then ((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) by A15, FDIFF_3:12;
then ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) . x) + ((f1 . x) * ((f2 `\ I) . x)) by A11, A8, VALUED_1:def 4;
then ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) . x) + ((f1 (#) (f2 `\ I)) . x) by A11, A8, VALUED_1:def 4;
hence ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x by A11, A9, VALUED_1:def 1; :: thesis: verum

end;

suppose A16: ( x <> inf I & x <> sup I ) ; :: thesis: ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x

then x in J by A11, Th3;
then A17: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A1, A2, FDIFF_1:9;
( (f1 `\ I) . x = diff (f1,x) & (f2 `\ I) . x = diff (f2,x) & ((f1 (#) f2) `\ I) . x = diff ((f1 (#) f2),x) ) by A1, A2, A5, A11, A16, Def2;
then ((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) by A17, FDIFF_1:16;
then ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) . x) + ((f1 . x) * ((f2 `\ I) . x)) by A11, A8, VALUED_1:def 4;
then ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) . x) + ((f1 (#) (f2 `\ I)) . x) by A11, A8, VALUED_1:def 4;
hence ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x by A11, A9, VALUED_1:def 1; :: thesis: verum

end;

end;

end;

hence (f1 (#) f2) `\ I = (f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I)) by A6, A9, PARTFUN1:5; :: thesis: for x being Real st x in I holds
((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x))

hereby :: thesis: verum

let x be Real; :: thesis: ( x in I implies ((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) )
assume A18: x in I ; :: thesis: ((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x))
then ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I))) . x by A6, A10;
then ((f1 (#) f2) `\ I) . x = ((f2 (#) (f1 `\ I)) . x) + ((f1 (#) (f2 `\ I)) . x) by A18, A9, VALUED_1:def 1;
then ((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 (#) (f2 `\ I)) . x) by A18, A8, VALUED_1:def 4;
hence ((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) by A18, A8, VALUED_1:def 4; :: thesis: verum

end;