theorem MoreDom: :: RVSUM_3:18

for f being real-valued FinSequence holds MeanMore f c= dom f