theorem Th19: :: ZMATRLIN:19

for V1 being free finite-rank Z_Module
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