let f be FinSequence; :: thesis: f | (len f) = f

f | (len f) = f | (Seg (len f)) by FINSEQ_1:def 15;

hence f | (len f) = f by FINSEQ_2:20; :: thesis: verum

f | (len f) = f | (Seg (len f)) by FINSEQ_1:def 15;

hence f | (len f) = f by FINSEQ_2:20; :: thesis: verum