theorem Th41: :: PDIFF_7:41

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for g being PartFunc of REAL,REAL
for x, y being Element of REAL m
for i being Nat
for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,y,i)