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