theorem Th64: :: HFDIFF_1:64

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