theorem Th12: :: PDIFF_9:12

for i, j being Element of NAT
for x being Element of REAL j holds x = (reproj (i,x)) . ((proj (i,j)) . x)