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 ^2 ),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) ^2 ))
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_on 2,Z implies (diff (f ^2 ),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) ^2 )) )
assume f is_differentiable_on 2,Z ; :: thesis: (diff (f ^2 ),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) ^2 ))
then (diff (f ^2 ),Z) . 2 = (((diff f,Z) . 2) (#) f) + ((2 (#) ((f `| Z) (#) (f `| Z))) + (f (#) ((diff f,Z) . 2))) by Th50
.= ((((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 Th5
.= (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z)))
.= (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) ^2 )) ;
hence (diff (f ^2 ),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) ^2 )) ; :: thesis: verum