theorem Th30: :: PDIFF_6:30

for X being set
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )