theorem Th1: :: MATRTOP3:1

for n being Nat
for K being Field
for M being Matrix of n,K
for P being Permutation of (Seg n) holds
( Det ((((M * P) @) * P) @) = Det M & ( for i, j being Nat st [i,j] in Indices M holds
((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) ) )