let n be natural number ; :: thesis: for Lv being Linear_Combination of RealVectSpace (Seg n)
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
set V = RealVectSpace (Seg n);
set T = TOP-REAL n;
let Lv be Linear_Combination of RealVectSpace (Seg n); :: thesis: for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
let Lr be Linear_Combination of TOP-REAL n; :: thesis: ( Lr = Lv implies Sum Lr = Sum Lv )
assume A1: Lr = Lv ; :: thesis: Sum Lr = Sum Lv
consider F being FinSequence of the carrier of (TOP-REAL n) such that
A2: ( F is one-to-one & rng F = Carrier Lr ) and
A3: Sum Lr = Sum (Lr (#) F) by RLVECT_2:def 8;
reconsider F1 = F as FinSequence of the carrier of (RealVectSpace (Seg n)) by Lm1;
A4: Lr (#) F = Lv (#) F1 by A1, Th18;
thus Sum Lv = Sum (Lv (#) F1) by A1, A2, RLVECT_2:def 8
.= Sum Lr by A3, A4, Th19 ; :: thesis: verum