theorem Th4: :: RLVECT_5:4

for V being RealLinearSpace
for L being Linear_Combination of V
for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)