for q being FinSubsequence
for k, n being Element of NAT st dom q c= Seg k & n > k holds
ex p being FinSequence st
( q c= p & dom p = Seg n )