let n be Nat; :: thesis: for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let Lv be Linear_Combination of n -VectSp_over F_Real; :: 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 (n -VectSp_over F_Real) by Lm1;
A4: Lr (#) F = Lv (#) F1 by A1, Th3;
Carrier Lr = Carrier Lv by A1, Th2;
hence Sum Lv = Sum (Lv (#) F1) by A2, VECTSP_6:def 6
.= Sum Lr by A3, A4, Th4 ;
:: thesis: verum