let Z be open Subset of REAL; for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z holds
(diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z implies (diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2)) )
assume that
A1:
f1 is_differentiable_on 2,Z
and
A2:
f2 is_differentiable_on 2,Z
; (diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))
(diff (f1,Z)) . 0 is_differentiable_on Z
by A1;
then
f1 | Z is_differentiable_on Z
by TAYLOR_1:def 5;
then A3:
f1 is_differentiable_on Z
by Th6;
A4: (diff (f1,Z)) . 2 =
(diff (f1,Z)) . (1 + 1)
.=
((diff (f1,Z)) . (1 + 0)) `| Z
by TAYLOR_1:def 5
.=
(((diff (f1,Z)) . 0) `| Z) `| Z
by TAYLOR_1:def 5
.=
((f1 | Z) `| Z) `| Z
by TAYLOR_1:def 5
.=
(f1 `| Z) `| Z
by A3, FDIFF_2:16
;
(diff (f2,Z)) . 0 is_differentiable_on Z
by A2;
then
f2 | Z is_differentiable_on Z
by TAYLOR_1:def 5;
then A5:
f2 is_differentiable_on Z
by Th6;
then A6:
f1 (#) f2 is_differentiable_on Z
by A3, FDIFF_2:20;
(diff (f2,Z)) . 1 =
(diff (f2,Z)) . (1 + 0)
.=
((diff (f2,Z)) . 0) `| Z
by TAYLOR_1:def 5
.=
(f2 | Z) `| Z
by TAYLOR_1:def 5
.=
f2 `| Z
by A5, FDIFF_2:16
;
then A7:
f2 `| Z is_differentiable_on Z
by A2;
then A8:
f1 (#) (f2 `| Z) is_differentiable_on Z
by A3, FDIFF_2:20;
(diff (f1,Z)) . 1 =
(diff (f1,Z)) . (1 + 0)
.=
((diff (f1,Z)) . 0) `| Z
by TAYLOR_1:def 5
.=
(f1 | Z) `| Z
by TAYLOR_1:def 5
.=
f1 `| Z
by A3, FDIFF_2:16
;
then A9:
f1 `| Z is_differentiable_on Z
by A1;
then A10:
(f1 `| Z) (#) f2 is_differentiable_on Z
by A5, FDIFF_2:20;
A11: (diff (f2,Z)) . 2 =
(diff (f2,Z)) . (1 + 1)
.=
((diff (f2,Z)) . (1 + 0)) `| Z
by TAYLOR_1:def 5
.=
(((diff (f2,Z)) . 0) `| Z) `| Z
by TAYLOR_1:def 5
.=
((f2 | Z) `| Z) `| Z
by TAYLOR_1:def 5
.=
(f2 `| Z) `| Z
by A5, FDIFF_2:16
;
(diff ((f1 (#) f2),Z)) . 2 =
(diff ((f1 (#) f2),Z)) . (1 + 1)
.=
((diff ((f1 (#) f2),Z)) . (1 + 0)) `| Z
by TAYLOR_1:def 5
.=
(((diff ((f1 (#) f2),Z)) . 0) `| Z) `| Z
by TAYLOR_1:def 5
.=
(((f1 (#) f2) | Z) `| Z) `| Z
by TAYLOR_1:def 5
.=
((f1 (#) f2) `| Z) `| Z
by A6, FDIFF_2:16
.=
(((f1 `| Z) (#) f2) + (f1 (#) (f2 `| Z))) `| Z
by A3, A5, FDIFF_2:20
.=
(((f1 `| Z) (#) f2) `| Z) + ((f1 (#) (f2 `| Z)) `| Z)
by A10, A8, FDIFF_2:17
.=
((((f1 `| Z) `| Z) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + ((f1 (#) (f2 `| Z)) `| Z)
by A5, A9, FDIFF_2:20
.=
((((diff (f1,Z)) . 2) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + (((f1 `| Z) (#) (f2 `| Z)) + (f1 (#) ((diff (f2,Z)) . 2)))
by A3, A7, A4, A11, FDIFF_2:20
.=
(((((diff (f1,Z)) . 2) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + ((f1 `| Z) (#) (f2 `| Z))) + (f1 (#) ((diff (f2,Z)) . 2))
by RFUNCT_1:8
.=
((((diff (f1,Z)) . 2) (#) f2) + (((f1 `| Z) (#) (f2 `| Z)) + ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))
by RFUNCT_1:8
.=
((((diff (f1,Z)) . 2) (#) f2) + ((1 (#) ((f1 `| Z) (#) (f2 `| Z))) + ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))
by RFUNCT_1:21
.=
((((diff (f1,Z)) . 2) (#) f2) + ((1 (#) ((f1 `| Z) (#) (f2 `| Z))) + (1 (#) ((f1 `| Z) (#) (f2 `| Z))))) + (f1 (#) ((diff (f2,Z)) . 2))
by RFUNCT_1:21
.=
((((diff (f1,Z)) . 2) (#) f2) + ((1 + 1) (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))
by Th5
.=
((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))
;
hence
(diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))
; verum