let f, g be FinSequence; :: thesis: (f ^ g) | (len f) = f
thus f = f | (len f) by FINSEQ_2:20
.= (f ^ g) | (len f) by Th22 ; :: thesis: verum