theorem :: FINSEQ_6:126

for p being FinSequence
for k1, k2 being Nat st k1 < k2 & k1 in dom p holds
mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2))