let A be open Subset of REAL; 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; ( 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
; ( 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 for x0 being Element of REAL st x0 in A holds
((f1 (#) f2) `| A) . x0 = (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) . x0let x0 be
Element of
REAL ;
( x0 in A implies ((f1 (#) f2) `| A) . x0 = (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) . x0 )assume A9:
x0 in A
;
((f1 (#) f2) `| A) . x0 = (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) . x0hence ((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
;
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; verum