theorem :: FINSEQ_5:7

for f being non empty FinSequence ex i being Nat st i + 1 = len f by NAT_1:6;