let k be Nat; :: thesis: for p, q being FinSequence st k in dom p & (len p) + 1 = len q holds

k + 1 in dom q

let p, q be FinSequence; :: thesis: ( k in dom p & (len p) + 1 = len q implies k + 1 in dom q )

assume that

A1: k in dom p and

A2: (len p) + 1 = len q ; :: thesis: k + 1 in dom q

k <= len p by A1, FINSEQ_3:25;

then ( 1 + 0 <= k + 1 & k + 1 <= (len p) + 1 ) by XREAL_1:7;

hence k + 1 in dom q by A2, FINSEQ_3:25; :: thesis: verum

k + 1 in dom q

let p, q be FinSequence; :: thesis: ( k in dom p & (len p) + 1 = len q implies k + 1 in dom q )

assume that

A1: k in dom p and

A2: (len p) + 1 = len q ; :: thesis: k + 1 in dom q

k <= len p by A1, FINSEQ_3:25;

then ( 1 + 0 <= k + 1 & k + 1 <= (len p) + 1 ) by XREAL_1:7;

hence k + 1 in dom q by A2, FINSEQ_3:25; :: thesis: verum