theorem Th40: :: PDIFF_7:40

for m being non zero Nat
for f being PartFunc of (REAL m),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 holds
reproj (i,x) = reproj (i,y)