theorem Th21: :: PDIFF_8:21

for m, n being non zero Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m) st X is open holds
( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for j being Nat st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )