theorem :: MATRTOP1:21

for n, m being Nat
for f being b₁ -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is b₁ -element FinSequence of REAL )