let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL , REAL st f is_differentiable_on 2,Z holds
(diff (f (#) f),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z)))
let f be PartFunc of REAL , REAL ; :: thesis: ( f is_differentiable_on 2,Z implies (diff (f (#) f),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z))) )
assume A1: f is_differentiable_on 2,Z ; :: thesis: (diff (f (#) f),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z)))
(diff (f (#) f),Z) . 2 = (((diff f,Z) . 2) (#) f) + ((2 (#) ((f `| Z) (#) (f `| Z))) + (f (#) ((diff f,Z) . 2))) by ThB3, A1
.= ((((diff f,Z) . 2) (#) f) + (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z))) by RFUNCT_1:19
.= ((1 (#) (f (#) ((diff f,Z) . 2))) + (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z))) by RFUNCT_1:33
.= ((1 (#) (f (#) ((diff f,Z) . 2))) + (1 (#) (f (#) ((diff f,Z) . 2)))) + (2 (#) ((f `| Z) (#) (f `| Z))) by RFUNCT_1:33
.= ((1 + 1) (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z))) by ThB2
.= (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z))) ;
hence (diff (f (#) f),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z))) ; :: thesis: verum