let f be FinSequence; :: thesis: for i being Nat holds len (f | i) <= len f
let i be Nat; :: thesis: len (f | i) <= len f
( i <= len f implies len (f | i) = i ) by FINSEQ_1:59;
hence len (f | i) <= len f by FINSEQ_1:58; :: thesis: verum