let p, q be FinSequence; :: thesis: ( len p = (len q) + 1 implies for i being Nat holds
( i in dom q iff ( i in dom p & i + 1 in dom p ) ) )
assume A1: len p = (len q) + 1 ; :: thesis: for i being Nat holds
( i in dom q iff ( i in dom p & i + 1 in dom p ) )
let i be Nat; :: thesis: ( i in dom q iff ( i in dom p & i + 1 in dom p ) )

hereby :: thesis: ( i in dom p & i + 1 in dom p implies i in dom q )

assume A2: i in dom q ; :: thesis: ( i in dom p & i + 1 in dom p )
then A3: i >= 1 by FINSEQ_3:25;
A4: i <= len q by A2, FINSEQ_3:25;
len q <= len p by A1, NAT_1:11;
then A5: ( i + 1 >= 1 & i <= len p ) by A4, NAT_1:11, XXREAL_0:2;
i + 1 <= len p by A1, A4, XREAL_1:6;
hence ( i in dom p & i + 1 in dom p ) by A3, A5, FINSEQ_3:25; :: thesis: verum

end;

assume that
A6: i in dom p and
A7: i + 1 in dom p ; :: thesis: i in dom q
i + 1 <= len p by A7, FINSEQ_3:25;
then A8: i <= len q by A1, XREAL_1:6;
i >= 1 by A6, FINSEQ_3:25;
hence i in dom q by A8, FINSEQ_3:25; :: thesis: verum