theorem LessDom: :: RVSUM_3:17

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