for n being Nat
for Lv being Linear_Combination of RealVectSpace (Seg n)
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv