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 that
A1: not k in dom p and
A2: k + 1 in dom p ; :: thesis: k = 0
A3: k + 1 <= len p by A2, FINSEQ_3:25;

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

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 A3, NAT_1:13; :: thesis: verum

end;

end;