:: deftheorem defines XFS2FS RVSUM_4:def 12 :
for D being set
for f being XFinSequence of D holds XFS2FS f = Shift (f,1);