:: deftheorem defines FS2XFS RVSUM_4:def 13 :
for D being set
for f being FinSequence of D holds FS2XFS f = (<%> D) ^ f;