theorem :: REAL_NS2:24

for n being Nat
for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds
Sum Lr = Sum Lv