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
Sum Lr = Sum 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
Sum Lr = Sum Lv
let Lr be Linear_Combination of REAL-NS n; :: thesis: ( Lr = Lv implies Sum Lr = Sum Lv )
assume A1: Lr = Lv ; :: thesis: Sum Lr = Sum Lv
reconsider Lt = Lr as Linear_Combination of TOP-REAL n by Th11;
Sum Lt = Sum Lr by Th23;
hence Sum Lr = Sum Lv by A1, MATRTOP2:5; :: thesis: verum