let Z be open Subset of REAL; 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; ( 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
; (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))
; verum