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

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