theorem Th12: :: PDIFF_1:12

for n being non zero Nat
for i being Nat
for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
(reproj (i,y)) * (proj (1,1)) = reproj (i,x)