let f be FinSequence; :: thesis: for n being Nat st n in dom f & n > 1 holds
n - 1 in dom f
consider l being Nat such that
A1: dom f = Seg l by FINSEQ_1:def 2;
thus for n being Nat st n in dom f & n > 1 holds
n - 1 in dom f by A1, FINSEQ_3:12; :: thesis: verum