theorem Th28: :: NDIFF_4:28

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