let p be FinSequence; :: thesis: for k being Nat st k + 1 in dom p & not k in dom p holds
k = 0
let k be Nat; :: thesis: ( k + 1 in dom p & not k in dom p implies k = 0 )
assume that
A1: k + 1 in dom p and
A2: not k in dom p ; :: thesis: k = 0
assume k <> 0 ; :: thesis: contradiction
then A3: k >= 1 by NAT_1:14;
( k <= k + 1 & k + 1 <= len p ) by A1, FINSEQ_3:25, NAT_1:12;
then k <= len p by XXREAL_0:2;
hence contradiction by A2, A3, FINSEQ_3:25; :: thesis: verum