for e being FinSequence of REAL
for f being FinSequence of F_Real st e = f holds
Sum e = Sum f