for F being FinSequence of F_Real
for G being FinSequence of F_Rat st F = G holds
Sum F = Sum G