let n be Nat; :: thesis: for K being commutative Ring
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
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
let K be commutative Ring; :: 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
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
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
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
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
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
let Perm be Permutation of (Seg n); :: thesis: for q being Element of Permutations n st q = p * (Perm ") holds
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
let q be Element of Permutations n; :: thesis: ( q = p * (Perm ") implies Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm )
assume A1: q = p * (Perm ") ; :: thesis: Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
reconsider perm = Perm as Element of Permutations n by MATRIX_1:def 12;
set Ap = A * Perm;
set P2 = Path_matrix (q,A);
set P1 = Path_matrix (p,(A * Perm));
A2: dom perm = Seg n by FUNCT_2:52;
A3: p is Permutation of (Seg n) by MATRIX_1:def 12;
then A4: dom p = Seg n by FUNCT_2:52;
A5: rng p = Seg n by A3, FUNCT_2:def 3;
A6: q is Permutation of (Seg n) by MATRIX_1:def 12;
then A7: dom q = Seg n by FUNCT_2:52;
len (Path_matrix (q,A)) = n by MATRIX_3:def 7;
then A8: dom (Path_matrix (q,A)) = Seg n by FINSEQ_1:def 3;
A9: rng perm = Seg n by FUNCT_2:def 3;
then A10: dom ((Path_matrix (q,A)) * perm) = Seg n by A2, A8, RELAT_1:27;
then reconsider P2p = (Path_matrix (q,A)) * perm as FinSequence by FINSEQ_1:def 2;
A11: len (Path_matrix (p,(A * Perm))) = n by MATRIX_3:def 7;
A12: rng q = Seg n by A6, FUNCT_2:def 3;

A13: now :: thesis: for k being Nat st 1 <= k & k <= len (Path_matrix (p,(A * Perm))) holds
P2p . k = (Path_matrix (p,(A * Perm))) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (Path_matrix (p,(A * Perm))) implies P2p . k = (Path_matrix (p,(A * Perm))) . k )
assume that
A14: 1 <= k and
A15: k <= len (Path_matrix (p,(A * Perm))) ; :: thesis: P2p . k = (Path_matrix (p,(A * Perm))) . k
A16: k in Seg n by A11, A14, A15;
then A17: p . k in Seg n by A4, A5, FUNCT_1:3;
then reconsider pk = p . k as Element of NAT ;
A18: k = (perm ") . (perm . k) by A2, A16, FUNCT_1:34;
[k,pk] in [:(Seg n),(Seg n):] by A16, A17, ZFMISC_1:87;
then [k,pk] in Indices A by MATRIX_0:24;
then consider permk being Nat such that
A19: perm . k = permk and
A20: [permk,pk] in Indices A and
A21: (A * Perm) * (k,pk) = A * (permk,pk) by Th37;
dom P2p = Seg n by A2, A9, A8, RELAT_1:27;
then A22: P2p . k = (Path_matrix (q,A)) . permk by A16, A19, FUNCT_1:12;
Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A23: permk in Seg n by A20, ZFMISC_1:87;
then q . permk in Seg n by A7, A12, FUNCT_1:3;
then reconsider qpermk = q . permk as Element of NAT ;
A24: (Path_matrix (q,A)) . permk = A * (permk,qpermk) by A8, A23, MATRIX_3:def 7;
A25: dom (Path_matrix (p,(A * Perm))) = Seg n by A11, FINSEQ_1:def 3;
q . permk = p . ((perm ") . (perm . k)) by A1, A7, A19, A23, FUNCT_1:12;
hence P2p . k = (Path_matrix (p,(A * Perm))) . k by A16, A21, A24, A22, A18, A25, MATRIX_3:def 7; :: thesis: verum

end;

n is Element of NAT by ORDINAL1:def 12;
then len P2p = n by A10, FINSEQ_1:def 3;
hence Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm by A11, A13, FINSEQ_1:14; :: thesis: verum