theorem :: NDIFF_4:26

for i being Element of NAT
for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being Real st 1 <= i & i <= n & f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )