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 A1:
( f1 is_differentiable_on A & f2 is_differentiable_on A )
; :: thesis: ( f1 (#) f2 is_differentiable_on A & (f1 (#) f2) `| A = ((f1 `| A) (#) f2) + (f1 (#) (f2 `| A)) )
then A2:
A c= dom f1
by FDIFF_1:def 7;
A3:
A c= dom f2
by A1, FDIFF_1:def 7;
then
A c= (dom f1) /\ (dom f2)
by A2, XBOOLE_1:19;
then A4:
A c= dom (f1 (#) f2)
by VALUED_1:def 4;
then
( f1 (#) f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds
((f1 (#) f2) `| A) . x0 = ((f2 . x0) * (diff f1,x0)) + ((f1 . x0) * (diff f2,x0)) ) )
by A1, FDIFF_1:29;
then A5:
dom ((f1 (#) f2) `| A) = A
by FDIFF_1:def 8;
dom (f1 `| A) = A
by A1, FDIFF_1:def 8;
then
(dom (f1 `| A)) /\ (dom f2) = A
by A3, XBOOLE_1:28;
then A6:
dom ((f1 `| A) (#) f2) = A
by VALUED_1:def 4;
dom (f2 `| A) = A
by A1, FDIFF_1:def 8;
then
(dom f1) /\ (dom (f2 `| A)) = A
by A2, XBOOLE_1:28;
then
dom (f1 (#) (f2 `| A)) = A
by VALUED_1:def 4;
then
(dom ((f1 `| A) (#) f2)) /\ (dom (f1 (#) (f2 `| A))) = A
by A6;
then A7:
dom (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) = A
by VALUED_1:def 1;
now let x0 be
Real;
:: thesis: ( x0 in A implies ((f1 (#) f2) `| A) . x0 = (((f1 `| A) (#) f2) + (f1 (#) (f2 `| A))) . x0 )assume A8:
x0 in A
;
:: thesis: ((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, A4, FDIFF_1:29
.=
(((f1 `| A) . x0) * (f2 . x0)) + ((f1 . x0) * (diff f2,x0))
by A1, A8, FDIFF_1:def 8
.=
(((f1 `| A) . x0) * (f2 . x0)) + ((f1 . x0) * ((f2 `| A) . x0))
by A1, A8, FDIFF_1:def 8
.=
(((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 A7, A8, 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, A4, A5, A7, FDIFF_1:29, PARTFUN1:34; :: thesis: verum