let Z be open Subset of REAL; for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 3,Z & f2 is_differentiable_on 3,Z holds
(diff ((f1 (#) f2),Z)) . 3 = ((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3))
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_differentiable_on 3,Z & f2 is_differentiable_on 3,Z implies (diff ((f1 (#) f2),Z)) . 3 = ((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3)) )
assume that
A1:
f1 is_differentiable_on 3,Z
and
A2:
f2 is_differentiable_on 3,Z
; (diff ((f1 (#) f2),Z)) . 3 = ((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3))
A3:
f2 is_differentiable_on Z
by A2, Th7;
set g2 = (diff (f2,Z)) . 2;
set g1 = (diff (f1,Z)) . 2;
(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 A3, FDIFF_2:16
;
then A4:
f2 `| Z is_differentiable_on Z
by A2;
A5:
( f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z )
by A1, A2, TAYLOR_1:23;
A6:
f1 is_differentiable_on Z
by A1, Th7;
A7:
(diff (f1,Z)) . 2 is_differentiable_on Z
by A1;
then A8:
((diff (f1,Z)) . 2) (#) f2 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 A6, FDIFF_2:16
;
then A9:
f1 `| Z is_differentiable_on Z
by A1;
then A10:
(f1 `| Z) (#) (f2 `| Z) is_differentiable_on Z
by A4, FDIFF_2:20;
then A11:
2 (#) ((f1 `| Z) (#) (f2 `| Z)) is_differentiable_on Z
by FDIFF_2:19;
then A12:
(((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z))) is_differentiable_on Z
by A8, FDIFF_2:17;
A13:
(diff (f2,Z)) . 2 is_differentiable_on Z
by A2;
then A14:
f1 (#) ((diff (f2,Z)) . 2) is_differentiable_on Z
by A6, FDIFF_2:20;
(diff ((f1 (#) f2),Z)) . 3 =
(diff ((f1 (#) f2),Z)) . (2 + 1)
.=
((diff ((f1 (#) f2),Z)) . 2) `| Z
by TAYLOR_1:def 5
.=
(((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))) `| Z
by A5, Th50
.=
(((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) `| Z) + ((f1 (#) ((diff (f2,Z)) . 2)) `| Z)
by A14, A12, FDIFF_2:17
.=
(((((diff (f1,Z)) . 2) (#) f2) `| Z) + ((2 (#) ((f1 `| Z) (#) (f2 `| Z))) `| Z)) + ((f1 (#) ((diff (f2,Z)) . 2)) `| Z)
by A8, A11, FDIFF_2:17
.=
(((((diff (f1,Z)) . 2) (#) f2) `| Z) + (2 (#) (((f1 `| Z) (#) (f2 `| Z)) `| Z))) + ((f1 (#) ((diff (f2,Z)) . 2)) `| Z)
by A10, FDIFF_2:19
.=
((((((diff (f1,Z)) . 2) `| Z) (#) f2) + (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) (((f1 `| Z) (#) (f2 `| Z)) `| Z))) + ((f1 (#) ((diff (f2,Z)) . 2)) `| Z)
by A3, A7, FDIFF_2:20
.=
((((((diff (f1,Z)) . 2) `| Z) (#) f2) + (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) (((f1 `| Z) (#) (f2 `| Z)) `| Z))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) (((diff (f2,Z)) . 2) `| Z)))
by A6, A13, FDIFF_2:20
.=
(((((diff (f1,Z)) . (2 + 1)) (#) f2) + (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) (((f1 `| Z) (#) (f2 `| Z)) `| Z))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) (((diff (f2,Z)) . 2) `| Z)))
by TAYLOR_1:def 5
.=
(((((diff (f1,Z)) . 3) (#) f2) + (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) (((f1 `| Z) (#) (f2 `| Z)) `| Z))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . (2 + 1))))
by TAYLOR_1:def 5
.=
(((((diff (f1,Z)) . 3) (#) f2) + (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) ((((f1 `| Z) `| Z) (#) (f2 `| Z)) + ((f1 `| Z) (#) ((f2 `| Z) `| Z))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by A9, A4, FDIFF_2:20
.=
(((((diff (f1,Z)) . 3) (#) f2) + (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) ((((diff (f1,Z)) . 2) (#) (f2 `| Z)) + ((f1 `| Z) (#) ((f2 `| Z) `| Z))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by A1, Lm3, Th7
.=
(((((diff (f1,Z)) . 3) (#) f2) + (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) ((((diff (f1,Z)) . 2) (#) (f2 `| Z)) + ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by A2, Lm3, Th7
.=
(((((diff (f1,Z)) . 3) (#) f2) + ((1 (#) ((diff (f1,Z)) . 2)) (#) (f2 `| Z))) + (2 (#) ((((diff (f1,Z)) . 2) (#) (f2 `| Z)) + ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by RFUNCT_1:21
.=
(((((diff (f1,Z)) . 3) (#) f2) + ((1 (#) ((diff (f1,Z)) . 2)) (#) (f2 `| Z))) + ((2 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by RFUNCT_1:16
.=
((((diff (f1,Z)) . 3) (#) f2) + (((1 (#) ((diff (f1,Z)) . 2)) (#) (f2 `| Z)) + ((2 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2)))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by RFUNCT_1:8
.=
((((diff (f1,Z)) . 3) (#) f2) + ((((1 (#) ((diff (f1,Z)) . 2)) (#) (f2 `| Z)) + (2 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z)))) + (2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by RFUNCT_1:8
.=
((((diff (f1,Z)) . 3) (#) f2) + (((1 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z)))) + (2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by RFUNCT_1:12
.=
((((diff (f1,Z)) . 3) (#) f2) + (((1 + 2) (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))
by Th5
.=
(((diff (f1,Z)) . 3) (#) f2) + (((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2)))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3))))
by RFUNCT_1:8
.=
(((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + ((2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))) + (((f1 `| Z) (#) ((diff (f2,Z)) . 2)) + (f1 (#) ((diff (f2,Z)) . 3)))))
by RFUNCT_1:8
.=
(((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (((2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))) + ((f1 `| Z) (#) ((diff (f2,Z)) . 2))) + (f1 (#) ((diff (f2,Z)) . 3))))
by RFUNCT_1:8
.=
(((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (((2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))) + (1 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2)))) + (f1 (#) ((diff (f2,Z)) . 3))))
by RFUNCT_1:21
.=
(((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (((2 + 1) (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))) + (f1 (#) ((diff (f2,Z)) . 3))))
by Th5
.=
(((diff (f1,Z)) . 3) (#) f2) + (((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2)))) + (f1 (#) ((diff (f2,Z)) . 3)))
by RFUNCT_1:8
.=
((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3))
by RFUNCT_1:8
;
hence
(diff ((f1 (#) f2),Z)) . 3 = ((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3))
; verum