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

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