let T be RealLinearSpace; :: thesis: for Lv being Linear_Combination of RLSp2RVSp T
for Lr being Linear_Combination of T st Lr = Lv holds
Sum Lr = Sum Lv
let Lv be Linear_Combination of RLSp2RVSp T; :: thesis: for Lr being Linear_Combination of T st Lr = Lv holds
Sum Lr = Sum Lv
let Lr be Linear_Combination of T; :: 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 T 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 (RLSp2RVSp T) ;
Carrier Lr = Carrier Lv by A1, Th73;
hence Sum Lv = Sum (Lv (#) F1) by A2, VECTSP_6:def 6
.= Sum Lr by A1, A3, Th74 ;
:: thesis: verum