theorem Th2: :: MATRTOP2:2

for n being Nat
for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Carrier Lr = Carrier Lv