theorem Th25: :: NDIFF_4:25

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