theorem Th30: :: NDIFF_4:30

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