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