theorem Th18: :: PDIFF_6:18

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n)