let r be Real; :: thesis: for V being RealLinearSpace
for L being Linear_Combination of V holds sum (r * L) = r * (sum L)
let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds sum (r * L) = r * (sum L)
let L be Linear_Combination of V; :: thesis: sum (r * L) = r * (sum L)
consider F being FinSequence of V such that
A1: F is one-to-one and
A2: rng F = Carrier L and
A3: sum L = Sum (L * F) by Def3;
L is Linear_Combination of Carrier L by RLVECT_2:def 6;
then r * L is Linear_Combination of Carrier L by RLVECT_2:44;
then A4: Carrier (r * L) c= rng F by A2, RLVECT_2:def 6;
thus r * (sum L) = Sum (r * (L * F)) by A3, RVSUM_1:87
.= Sum ((r * L) * F) by Th14
.= sum (r * L) by A1, A4, Th30 ; :: thesis: verum