theorem :: NDIFF_4:31

for X being set
for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * f is_differentiable_on X )