let n be Nat; :: thesis: for Lr being Linear_Combination of REAL-NS n
for Lt being Linear_Combination of TOP-REAL n st Lr = Lt holds
Sum Lr = Sum Lt
let Lr be Linear_Combination of REAL-NS n; :: thesis: for Lt being Linear_Combination of TOP-REAL n st Lr = Lt holds
Sum Lr = Sum Lt
let Lt be Linear_Combination of TOP-REAL n; :: thesis: ( Lr = Lt implies Sum Lr = Sum Lt )
assume A1: Lr = Lt ; :: thesis: Sum Lr = Sum Lt
set R = REAL-NS n;
set T = TOP-REAL n;
consider Ft being FinSequence of the carrier of (TOP-REAL n) such that
A2: ( Ft is one-to-one & rng Ft = Carrier Lt ) and
A3: Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def 8;
reconsider Fr = Ft as FinSequence of the carrier of (REAL-NS n) by Th4;
thus Sum Lt = Sum (Lr (#) Fr) by A1, A3, Th19, Th21
.= Sum Lr by A1, A2, RLVECT_2:def 8 ; :: thesis: verum