theorem :: RVSUM_4:35

for D being set
for f being XFinSequence
for g being FinSequence of D holds (f ^ g) /^ (len f) = FS2XFS g