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;
A4:
1 <= 3 - 1
;
(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 A5:
f2 `| Z is_differentiable_on Z
by A2, A4, TAYLOR_1:def 6;
A6:
( f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z )
by A1, A2, TAYLOR_1:23;
A7:
f1 is_differentiable_on Z
by A1, Th7;
A8:
2 <= 3 - 1
;
then A9:
(diff f1,Z) . 2 is_differentiable_on Z
by A1, TAYLOR_1:def 6;
then A10:
((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 A7, FDIFF_2:16
;
then A11:
f1 `| Z is_differentiable_on Z
by A1, A4, TAYLOR_1:def 6;
then A12:
(f1 `| Z) (#) (f2 `| Z) is_differentiable_on Z
by A5, FDIFF_2:20;
then A13:
2 (#) ((f1 `| Z) (#) (f2 `| Z)) is_differentiable_on Z
by FDIFF_2:19;
then A14:
(((diff f1,Z) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z))) is_differentiable_on Z
by A10, FDIFF_2:17;
A15:
(diff f2,Z) . 2 is_differentiable_on Z
by A2, A8, TAYLOR_1:def 6;
then A16:
f1 (#) ((diff f2,Z) . 2) is_differentiable_on Z
by A7, 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 A6, Th50
.=
(((((diff f1,Z) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) `| Z) + ((f1 (#) ((diff f2,Z) . 2)) `| Z)
by A16, A14, FDIFF_2:17
.=
(((((diff f1,Z) . 2) (#) f2) `| Z) + ((2 (#) ((f1 `| Z) (#) (f2 `| Z))) `| Z)) + ((f1 (#) ((diff f2,Z) . 2)) `| Z)
by A10, A13, FDIFF_2:17
.=
(((((diff f1,Z) . 2) (#) f2) `| Z) + (2 (#) (((f1 `| Z) (#) (f2 `| Z)) `| Z))) + ((f1 (#) ((diff f2,Z) . 2)) `| Z)
by A12, 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, A9, 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 A7, A15, 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 A11, A5, 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:33
.=
(((((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:28
.=
((((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:19
.=
((((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:19
.=
((((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:24
.=
((((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:19
.=
(((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:19
.=
(((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:19
.=
(((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:33
.=
(((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:19
.=
((((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:19
;
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