let n be Nat; :: thesis: for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds
Carrier Lr = Carrier Lv
let Lv be Linear_Combination of n -VectSp_over F_Real; :: thesis: for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds
Carrier Lr = Carrier Lv
let Lr be Linear_Combination of REAL-NS n; :: thesis: ( Lr = Lv implies Carrier Lr = Carrier Lv )
assume A1: Lr = Lv ; :: thesis: Carrier Lr = Carrier Lv
reconsider Lr1 = Lr as Linear_Combination of TOP-REAL n by Th11;
Carrier Lr1 = Carrier Lv by A1, MATRTOP2:2;
hence Carrier Lr = Carrier Lv ; :: thesis: verum