let Z be open Subset of REAL ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: (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: f1 is_differentiable_on 2,Z by A1, TAYLOR_1:23;
A4: f1 is_differentiable_on Z by A1, ThB19;
A5: f2 is_differentiable_on 2,Z by A2, TAYLOR_1:23;
A6: f2 is_differentiable_on Z by ThB19, A2;
A7: 2 <= 3 - 1 ;
then A8: (diff f1,Z) . 2 is_differentiable_on Z by A1, TAYLOR_1:def 6;
then A9: ((diff f1,Z) . 2) (#) f2 is_differentiable_on Z by A6, FDIFF_2:20;
A10: (diff f2,Z) . 2 is_differentiable_on Z by A2, A7, TAYLOR_1:def 6;
then A11: f1 (#) ((diff f2,Z) . 2) is_differentiable_on Z by A4, FDIFF_2:20;
A12: 1 <= 3 - 1 ;
(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 A14: f1 `| Z is_differentiable_on Z by A1, A12, TAYLOR_1:def 6;
(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 A6, FDIFF_2:16 ;
then A16: f2 `| Z is_differentiable_on Z by A2, A12, TAYLOR_1:def 6;
then A17: (f1 `| Z) (#) (f2 `| Z) is_differentiable_on Z by A14, FDIFF_2:20;
then A18: 2 (#) ((f1 `| Z) (#) (f2 `| Z)) is_differentiable_on Z by FDIFF_2:19;
then A19: (((diff f1,Z) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z))) is_differentiable_on Z by A9, FDIFF_2:17;
set g1 = (diff f1,Z) . 2;
set g2 = (diff f2,Z) . 2;
(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 ThB3, A3, A5
.= (((((diff f1,Z) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) `| Z) + ((f1 (#) ((diff f2,Z) . 2)) `| Z) by A19, A11, FDIFF_2:17
.= (((((diff f1,Z) . 2) (#) f2) `| Z) + ((2 (#) ((f1 `| Z) (#) (f2 `| Z))) `| Z)) + ((f1 (#) ((diff f2,Z) . 2)) `| Z) by A9, A18, FDIFF_2:17
.= (((((diff f1,Z) . 2) (#) f2) `| Z) + (2 (#) (((f1 `| Z) (#) (f2 `| Z)) `| Z))) + ((f1 (#) ((diff f2,Z) . 2)) `| Z) by A17, 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 A8, A6, 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 A4, A10, 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 A14, A16, 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 Lm1, A1, ThB19
.= (((((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 Lm1, ThB19, A2
.= (((((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 ThB2
.= (((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 ThB2
.= (((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)) ; :: thesis: verum