let n be Nat; :: thesis: for K being Field
for A being Matrix of n,K
for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm " ) holds
the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A)
let K be Field; :: thesis: for A being Matrix of n,K
for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm " ) holds
the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A)
let A be Matrix of n,K; :: thesis: for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm " ) holds
the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A)
let p be Element of Permutations n; :: thesis: for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm " ) holds
the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A)
let Perm be Permutation of (Seg n); :: thesis: for q being Element of Permutations n st q = p * (Perm " ) holds
the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A)
let q be Element of Permutations n; :: thesis: ( q = p * (Perm " ) implies the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A) )
assume A1: q = p * (Perm " ) ; :: thesis: the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A)
set mm = the multF of K;
set P2 = Path_matrix q,A;
set P1 = Path_matrix p,(A * Perm);

now

per cases ( n = 0 or n + 0 > 0 ) ;

case A2: n = 0 ; :: thesis: the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A)

then len (Path_matrix p,(A * Perm)) = 0 by MATRIX_3:def 7;
then A3: the multF of K $$ (Path_matrix p,(A * Perm)) = the_unity_wrt the multF of K by FINSOP_1:def 1;
len (Path_matrix q,A) = 0 by A2, MATRIX_3:def 7;
hence the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A) by A3, FINSOP_1:def 1; :: thesis: verum

end;

case n + 0 > 0 ; :: thesis: the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A)

then A4: n >= 1 by NAT_1:19;
A5: len (Path_matrix q,A) = n by MATRIX_3:def 7;
A6: Perm is Element of Permutations n by MATRIX_2:def 11;
Path_matrix p,(A * Perm) = (Path_matrix q,A) * Perm by A1, Th40;
hence the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A) by A4, A5, A6, MATRIX_7:33; :: thesis: verum

end;

end;

end;

hence the multF of K $$ (Path_matrix p,(A * Perm)) = the multF of K $$ (Path_matrix q,A) ; :: thesis: verum