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
thus f = f | (len f) by FINSEQ_2:20
.= (f ^ g) | (len f) by Th25 ; :: thesis: verum