let A be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds
( f1 (#) f2 is_differentiable_on A & (f1 (#) f2) `| A = ((f1 `| A) (#) f2) + (f1 (#) (f2 `| A)) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_differentiable_on A & f2 is_differentiable_on A implies ( f1 (#) f2 is_differentiable_on A & (f1 (#) f2) `| A = ((f1 `| A) (#) f2) + (f1 (#) (f2 `| A)) ) )
assume that
A1: f1 is_differentiable_on A and
A2: f2 is_differentiable_on A ; :: thesis: ( f1 (#) f2 is_differentiable_on A & (f1 (#) f2) `| A = ((f1 `| A) (#) f2) + (f1 (#) (f2 `| A)) )
A3: A c= dom f1 by A1;
A4: A c= dom f2 by A2;
then A c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
then A5: A c= dom (f1 (#) f2) by VALUED_1:def 4;
then f1 (#) f2 is_differentiable_on A by A1, A2, FDIFF_1:21;
then A6: dom ((f1 (#) f2) `| A) = A by FDIFF_1:def 7;
dom (f2 `| A) = A by A2, FDIFF_1:def 7;
then (dom f1) /\ (dom (f2 `| A)) = A by A3, XBOOLE_1:28;
then A7: dom (f1 (#) (f2 `| A)) = A by VALUED_1:def 4;
dom (f1 `| A) = A by A1, FDIFF_1:def 7;
then (dom (f1 `| A)) /\ (dom f2) = A by A4, XBOOLE_1:28;
then dom ((f1 `| A) (#) f2) = A by VALUED_1:def 4;
then (dom ((f1 `| A) (#) f2)) /\ (dom (f1 (#) (f2 `| A))) = A by A7;
then A8: dom (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) = A by VALUED_1:def 1;

now :: thesis: for x0 being Element of REAL st x0 in A holds
((f1 (#) f2) `| A) . x0 = (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) . x0

let x0 be Element of REAL ; :: thesis: ( x0 in A implies ((f1 (#) f2) `| A) . x0 = (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) . x0 )
assume A9: x0 in A ; :: thesis: ((f1 (#) f2) `| A) . x0 = (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) . x0
hence ((f1 (#) f2) `| A) . x0 = ((diff (f1,x0)) * (f2 . x0)) + ((f1 . x0) * (diff (f2,x0))) by A1, A2, A5, FDIFF_1:21
.= (((f1 `| A) . x0) * (f2 . x0)) + ((f1 . x0) * (diff (f2,x0))) by A1, A9, FDIFF_1:def 7
.= (((f1 `| A) . x0) * (f2 . x0)) + ((f1 . x0) * ((f2 `| A) . x0)) by A2, A9, FDIFF_1:def 7
.= (((f1 `| A) (#) f2) . x0) + ((f1 . x0) * ((f2 `| A) . x0)) by VALUED_1:5
.= (((f1 `| A) (#) f2) . x0) + ((f1 (#) (f2 `| A)) . x0) by VALUED_1:5
.= (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) . x0 by A8, A9, VALUED_1:def 1 ;
:: thesis: verum

end;

hence ( f1 (#) f2 is_differentiable_on A & (f1 (#) f2) `| A = ((f1 `| A) (#) f2) + (f1 (#) (f2 `| A)) ) by A1, A2, A5, A6, A8, FDIFF_1:21, PARTFUN1:5; :: thesis: verum