theorem Th29: :: NDIFF_4:29

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