theorem Th39: :: PDIFF_7:39

for m being non zero Nat
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
(proj (i,m)) . y = xi