theorem :: HFDIFF_1:20

for n being Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds
f1 - f2 is_differentiable_on n,Z