theorem :: FDIFF_1:21

for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 (#) f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 (#) f2) `| Z) . x = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x))) ) )