let D be set ; :: thesis: for f, g being FinSequence of D holds (f ^' g) | (len f) = f
let f, g be FinSequence of D; :: thesis: (f ^' g) | (len f) = f
f | (len f) = f | (Seg (len f)) by FINSEQ_1:def 16;
hence (f ^' g) | (len f) = f by Th49, FINSEQ_2:20; :: thesis: verum