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 9;
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