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.|