for F being FinSequence of ExtREAL
for f being FinSequence of REAL st F = f holds
Sum F = Sum f