theorem Th5: :: PDIFF_7:5

for i, j being Nat
for xi being Element of (REAL-NS 1) st 1 <= i & i <= j holds
||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = ||.xi.||