for k being Nat
for p being XFinSequence holds
( k < len p iff k in dom p ) by Lm1;