theorem :: FINSEQ_3:156

for p being FinSequence
for k being Nat st k in dom p holds
for i being Nat st 1 <= i & i <= k holds
i in dom p