theorem Th37: :: HFDIFF_1:37
for x being Real
for m being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((#Z m),Z)) . m) . x = m !