theorem :: RVSUM_4:37

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