let k be Nat; :: thesis: for p being FinSequence st k in dom p & not k + 1 in dom p holds
len p = k
let p be FinSequence; :: thesis: ( k in dom p & not k + 1 in dom p implies len p = k )
assume A: ( k in dom p & not k + 1 in dom p ) ; :: thesis: len p = k
B: ( 1 <= k & k <= len p ) by A, FINSEQ_3:27;
C: ( 1 > k + 1 or k + 1 > len p ) by A, FINSEQ_3:27;
1 + 0 <= k + 1 by XREAL_1:9;
hence len p = k by B, C, NAT_1:22; :: thesis: verum