for f being FinSequence of REAL
for m being Real holds Sum (((len f) |-> m) - f) = ((len f) * m) - (Sum f)