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))
A3:
0 <= 2 - 1
;
then
(diff f1,Z) . 0 is_differentiable_on Z
by A1, TAYLOR_1:def 6;
then
f1 | Z is_differentiable_on Z
by TAYLOR_1:def 5;
then A4:
f1 is_differentiable_on Z
by Th6;
A5: (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 A4, FDIFF_2:16
;
A6:
1 <= 2 - 1
;
(diff f2,Z) . 0 is_differentiable_on Z
by A2, A3, TAYLOR_1:def 6;
then
f2 | Z is_differentiable_on Z
by TAYLOR_1:def 5;
then A7:
f2 is_differentiable_on Z
by Th6;
then A8:
f1 (#) f2 is_differentiable_on Z
by A4, 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 A7, FDIFF_2:16
;
then A9:
f2 `| Z is_differentiable_on Z
by A2, A6, TAYLOR_1:def 6;
then A10:
f1 (#) (f2 `| Z) is_differentiable_on Z
by A4, 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 A4, FDIFF_2:16
;
then A11:
f1 `| Z is_differentiable_on Z
by A1, A6, TAYLOR_1:def 6;
then A12:
(f1 `| Z) (#) f2 is_differentiable_on Z
by A7, FDIFF_2:20;
A13: (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 A7, 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 A8, FDIFF_2:16
.=
(((f1 `| Z) (#) f2) + (f1 (#) (f2 `| Z))) `| Z
by A4, A7, FDIFF_2:20
.=
(((f1 `| Z) (#) f2) `| Z) + ((f1 (#) (f2 `| Z)) `| Z)
by A12, A10, FDIFF_2:17
.=
((((f1 `| Z) `| Z) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + ((f1 (#) (f2 `| Z)) `| Z)
by A7, A11, FDIFF_2:20
.=
((((diff f1,Z) . 2) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + (((f1 `| Z) (#) (f2 `| Z)) + (f1 (#) ((diff f2,Z) . 2)))
by A4, A9, A5, A13, FDIFF_2:20
.=
(((((diff f1,Z) . 2) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + ((f1 `| Z) (#) (f2 `| Z))) + (f1 (#) ((diff f2,Z) . 2))
by RFUNCT_1:19
.=
((((diff f1,Z) . 2) (#) f2) + (((f1 `| Z) (#) (f2 `| Z)) + ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff f2,Z) . 2))
by RFUNCT_1:19
.=
((((diff f1,Z) . 2) (#) f2) + ((1 (#) ((f1 `| Z) (#) (f2 `| Z))) + ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff f2,Z) . 2))
by RFUNCT_1:33
.=
((((diff f1,Z) . 2) (#) f2) + ((1 (#) ((f1 `| Z) (#) (f2 `| Z))) + (1 (#) ((f1 `| Z) (#) (f2 `| Z))))) + (f1 (#) ((diff f2,Z) . 2))
by RFUNCT_1:33
.=
((((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