let D be set ; :: thesis: for f being FinSequence of D holds f | (len f) = f
let f be FinSequence of D; :: 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:23; :: thesis: verum