theorem :: HFDIFF_1:66

for Z being 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))