for F being FinSequence of F_Real
for G being FinSequence of INT.Ring st F = G holds
Sum F = Sum G