theorem Th20: :: PDIFF_8:20

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)
for i being Nat st 1 <= i & i <= m & X is open holds
( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Nat st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )