theorem ZMATRLIN42: :: ZMODLAT2:46

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