let k be Nat; :: thesis: for p being FinSequence st not k in dom p & k + 1 in dom p holds
k = 0
let p be FinSequence; :: thesis: ( not k in dom p & k + 1 in dom p implies k = 0 )
assume A1: ( not k in dom p & k + 1 in dom p ) ; :: thesis: k = 0
then A2: ( 1 <= k + 1 & k + 1 <= len p ) by FINSEQ_3:27;

per cases ( k < 1 or k > len p ) by A1, FINSEQ_3:27;

suppose k < 1 ; :: thesis: k = 0

hence k = 0 by NAT_1:14; :: thesis: verum

end;

suppose k > len p ; :: thesis: k = 0

hence k = 0 by A2, NAT_1:13; :: thesis: verum

end;

end;