theorem :: FINSEQ_5:37

for f, g being FinSequence holds (f ^ g) /^ (len f) = g