for p being FinSequence of ExtREAL
for q being FinSequence of REAL st p = q holds
Sum p = Sum q by Th2;