let Z be open Subset of REAL ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: (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 A4: (diff f1,Z) . 0 is_differentiable_on Z by A1, TAYLOR_1:def 6;
f1 | Z is_differentiable_on Z by A4, TAYLOR_1:def 5;
then A6: f1 is_differentiable_on Z by ThB1;
A7: (diff f2,Z) . 0 is_differentiable_on Z by A2, A3, TAYLOR_1:def 6;
f2 | Z is_differentiable_on Z by A7, TAYLOR_1:def 5;
then A8: f2 is_differentiable_on Z by ThB1;
then A9: f1 (#) f2 is_differentiable_on Z by A6, FDIFF_2:20;
A10: 1 <= 2 - 1 ;
A12: (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 ;
A13: f1 `| Z is_differentiable_on Z by A1, A12, A10, TAYLOR_1:def 6;
then B1: (f1 `| Z) (#) f2 is_differentiable_on Z by A8, FDIFF_2:20;
A15: (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 A8, FDIFF_2:16 ;
A16: f2 `| Z is_differentiable_on Z by A2, A10, A15, TAYLOR_1:def 6;
then A17: f1 (#) (f2 `| Z) is_differentiable_on Z by A6, FDIFF_2:20;
A18: (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 A6, FDIFF_2:16 ;
A19: (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 A8, 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 A9, FDIFF_2:16
.= (((f1 `| Z) (#) f2) + (f1 (#) (f2 `| Z))) `| Z by A8, A6, FDIFF_2:20
.= (((f1 `| Z) (#) f2) `| Z) + ((f1 (#) (f2 `| Z)) `| Z) by A17, B1, FDIFF_2:17
.= ((((f1 `| Z) `| Z) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + ((f1 (#) (f2 `| Z)) `| Z) by A13, A8, FDIFF_2:20
.= ((((diff f1,Z) . 2) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + (((f1 `| Z) (#) (f2 `| Z)) + (f1 (#) ((diff f2,Z) . 2))) by A18, A19, A6, A16, 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 ThB2
.= ((((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)) ; :: thesis: verum