theorem Th124: :: FINSEQ_6:125

for f being FinSequence
for k being Nat
for p being set holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)