let p, q be FinSequence; :: thesis: ( len p = (len q) + 1 implies for i being Element of 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 Element of NAT holds
( i in dom q iff ( i in dom p & i + 1 in dom p ) )
let i be Element of 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 i in dom q ; :: thesis: ( i in dom p & i + 1 in dom p )
then A2: ( i >= 1 & i <= len q & len q <= len p ) by A1, FINSEQ_3:27, NAT_1:11;
then ( i + 1 <= len p & i + 1 >= 1 & i <= len p ) by A1, NAT_1:11, XREAL_1:8, XXREAL_0:2;
hence ( i in dom p & i + 1 in dom p ) by A2, FINSEQ_3:27; :: thesis: verum

end;

assume ( i in dom p & i + 1 in dom p ) ; :: thesis: i in dom q
then A3: ( i >= 1 & i + 1 <= len p ) by FINSEQ_3:27;
then i <= len q by A1, XREAL_1:8;
hence i in dom q by A3, FINSEQ_3:27; :: thesis: verum