theorem :: ABCMIZ_0:32

for p, q being FinSequence
for i being Nat st i >= 1 & i < len p holds
(p $^ q) . i = p . i