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
Path_matrix p,(A * Perm) = (Path_matrix q,A) * Perm
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
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_2:def 11;
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:67;
A3: p is Permutation of (Seg n) by MATRIX_2:def 11;
then A4: dom p = Seg n by FUNCT_2:67;
A5: rng p = Seg n by A3, FUNCT_2:def 3;
A6: q is Permutation of (Seg n) by MATRIX_2:def 11;
then A7: dom q = Seg n by FUNCT_2:67;
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:46;
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

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
k in NAT by ORDINAL1:def 13;
then A16: k in Seg n by A11, A14, A15;
then A17: p . k in Seg n by A4, A5, FUNCT_1:12;
then reconsider pk = p . k as Element of NAT ;
A18: k = (perm " ) . (perm . k) by A2, A16, FUNCT_1:56;
[k,pk] in [:(Seg n),(Seg n):] by A16, A17, ZFMISC_1:106;
then [k,pk] in Indices A by MATRIX_1:25;
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:46;
then A22: P2p . k = (Path_matrix q,A) . permk by A16, A19, FUNCT_1:22;
Indices A = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A23: permk in Seg n by A20, ZFMISC_1:106;
then q . permk in Seg n by A7, A12, FUNCT_1:12;
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:22;
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 13;
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:18; :: thesis: verum