:: deftheorem defines XFS2FS RVSUM_4:def 11 :
for D being set
for f being XFinSequence of D holds XFS2FS f = (<*> D) ^ f;