theorem Th13: :: PDIFF_1:13

for n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))