let n be Nat; :: thesis: for p being FinSequence holds
( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) )
let p be FinSequence; :: thesis: ( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) )
thus ( 1 <= n & n < len p implies ( n in dom p & n + 1 in dom p ) ) :: thesis: ( n in dom p & n + 1 in dom p implies ( 1 <= n & n < len p ) )

proof

assume that
A1: 1 <= n and
A2: n < len p ; :: thesis: ( n in dom p & n + 1 in dom p )
( 1 <= n + 1 & n + 1 <= len p ) by A2, NAT_1:11, NAT_1:13;
then A3: n + 1 in Seg (len p) by FINSEQ_1:1;
n in Seg (len p) by A1, A2, FINSEQ_1:1;
hence ( n in dom p & n + 1 in dom p ) by A3, FINSEQ_1:def 3; :: thesis: verum

end;

thus ( n in dom p & n + 1 in dom p implies ( 1 <= n & n < len p ) ) :: thesis: verum

proof

assume that
A4: n in dom p and
A5: n + 1 in dom p ; :: thesis: ( 1 <= n & n < len p )
n + 1 in Seg (len p) by A5, FINSEQ_1:def 3;
then A6: n + 1 <= len p by FINSEQ_1:1;
n in Seg (len p) by A4, FINSEQ_1:def 3;
hence ( 1 <= n & n < len p ) by A6, FINSEQ_1:1, NAT_1:13; :: thesis: verum

end;