theorem Th3: :: NDIFF_4:3

for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n)
for x being Real st h = f holds
diff (f,x) = diff (h,x)