theorem :: REAL_NS2:13

for n being Nat
for Lv being Linear_Combination of TOP-REAL n
for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds
Carrier Lr = Carrier Lv ;