for m, n being Nat
for p being b₂ -element FinSequence
for q being b₁ -element FinSequence holds (p ^ q) . (n + 1) = q . 1 & ... & (p ^ q) . (n + m) = q . m