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:8
.= ((1 (#) (f (#) ((diff (f,Z)) . 2))) + (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z))) by RFUNCT_1:21
.= ((1 (#) (f (#) ((diff (f,Z)) . 2))) + (1 (#) (f (#) ((diff (f,Z)) . 2)))) + (2 (#) ((f `| Z) (#) (f `| Z))) by RFUNCT_1:21
.= ((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