theorem Th1: :: VECTSP_9:1

for GF being Field
for V being VectSp of GF
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)