for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z holds
(diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))