theorem DSS: :: RVSUM_4:38

for D being set
for f being XFinSequence of D holds dom (Shift (f,1)) = Seg (len f)