theorem Th11: :: PDIFF_9:11

for j being Element of NAT
for q being Real
for i being Nat st 1 <= i & i <= j holds
|.((reproj (i,(0* j))) . q).| = |.q.|