theorem Th7: :: HFDIFF_1:7

for n being Element of NAT
for Z being open Subset of REAL
for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds
f1 is_differentiable_on Z