for n, k being Nat
for i1 being Element of n
for p being b₁ + b₂ -element XFinSequence st n <> 0 & k <> 0 holds
(p | n) . i1 = p . i1