theorem Th39: :: ORDEQ_01:39

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