let n be Nat; :: thesis: for L being Linear_Combination of REAL-NS n
for S being Linear_Combination of TOP-REAL n st L = S holds
sum L = sum S
let L be Linear_Combination of REAL-NS n; :: thesis: for S being Linear_Combination of TOP-REAL n st L = S holds
sum L = sum S
let S be Linear_Combination of TOP-REAL n; :: thesis: ( L = S implies sum L = sum S )
assume A1: L = S ; :: thesis: sum L = sum S
consider F being FinSequence of (REAL-NS n) such that
A2: ( F is one-to-one & rng F = Carrier L & sum L = Sum (L * F) ) by RLAFFIN1:def 3;
reconsider E = F as FinSequence of (TOP-REAL n) by Th4;
Sum (L * F) = Sum (S * E) by A1;
hence sum L = sum S by A2, A1, RLAFFIN1:def 3; :: thesis: verum