theorem :: MESFUNC3:18

for a being FinSequence of ExtREAL
for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds
a . n = p ) holds
Sum a = N * p by Lm1;