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 A: ( k in dom p & (len p) + 1 = len q ) ; :: thesis: k + 1 in dom q
( 1 <= k & k <= len p ) by A, FINSEQ_3:27;
then ( 1 + 0 <= k + 1 & k + 1 <= (len p) + 1 ) by XREAL_1:9;
hence k + 1 in dom q by A, FINSEQ_3:27; :: thesis: verum