theorem :: AFINSQ_1:73

for p being XFinSequence
for m being Nat st not m in dom p holds
not m + 1 in dom p