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 that
A1: k in dom p and
A2: not k + 1 in dom p ; :: thesis: len p = k
A3: ( 1 > k + 1 or k + 1 > len p ) by A2, FINSEQ_3:25;
A4: 1 + 0 <= k + 1 by XREAL_1:7;
k <= len p by A1, FINSEQ_3:25;
hence len p = k by A3, A4, NAT_1:22; :: thesis: verum