theorem Th19: :: MATRLIN:19

for K being Field
for V1 being finite-dimensional VectSp of K
for F, F1 being FinSequence of V1
for KL being Linear_Combination of V1
for p being Permutation of (dom F) st F1 = F * p holds
KL (#) F1 = (KL (#) F) * p