let n be Nat; :: thesis: for f being FinSequence holds
( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )
let f be FinSequence; :: thesis: ( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )
thus ( 1 <= n & n + 1 <= len f implies ( n in dom f & n + 1 in dom f ) ) :: thesis: ( n in dom f & n + 1 in dom f implies ( 1 <= n & n + 1 <= len f ) )
proof
assume that
A1: 1 <= n and
A2: n + 1 <= len f ; :: thesis: ( n in dom f & n + 1 in dom f )
n <= n + 1 by NAT_1:11;
then ( 1 <= n + 1 & n <= len f ) by A2, NAT_1:11, XXREAL_0:2;
hence ( n in dom f & n + 1 in dom f ) by A1, A2, FINSEQ_3:25; :: thesis: verum
end;
thus ( n in dom f & n + 1 in dom f implies ( 1 <= n & n + 1 <= len f ) ) by FINSEQ_3:25; :: thesis: verum