let n be Element of NAT ; :: thesis: for K being Field
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
Path_matrix (p " ),(A @ ) = (Path_matrix p,A) * (p " )
let K be Field; :: thesis: for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
Path_matrix (p " ),(A @ ) = (Path_matrix p,A) * (p " )
let p be Element of Permutations n; :: thesis: for A being Matrix of n,K st n >= 1 holds
Path_matrix (p " ),(A @ ) = (Path_matrix p,A) * (p " )
let A be Matrix of n,K; :: thesis: ( n >= 1 implies Path_matrix (p " ),(A @ ) = (Path_matrix p,A) * (p " ) )
assume A1: n >= 1 ; :: thesis: Path_matrix (p " ),(A @ ) = (Path_matrix p,A) * (p " )
set f = Path_matrix p,A;
A2: len (Path_matrix p,A) = n by MATRIX_3:def 7;
then Path_matrix p,A <> {} by A1;
then dom (Path_matrix p,A) <> {} ;
then A3: Seg n <> {} by A2, FINSEQ_1:def 3;
A4: p " is Permutation of (Seg n) by MATRIX_2:def 11;
reconsider fp = p " as Function of (Seg n),(Seg n) by MATRIX_2:def 11;
A5: p is Permutation of (Seg n) by MATRIX_2:def 11;
reconsider fp0 = p as Function of (Seg n),(Seg n) by MATRIX_2:def 11;
A6: rng fp = Seg n by A4, FUNCT_2:def 3;
then rng (p " ) c= dom (Path_matrix p,A) by A2, FINSEQ_1:def 3;
then A7: dom ((Path_matrix p,A) * (p " )) = dom fp by RELAT_1:46;
A8: dom fp = Seg n by A3, FUNCT_2:def 1;
reconsider m = (Path_matrix p,A) * (p " ) as FinSequence of K by A1, A2, Th34;
A9: len m = n by A7, A8, FINSEQ_1:def 3;
for i, j being Nat st i in dom m & j = (p " ) . i holds
m . i = (A @ ) * i,j

proof

let i, j be Nat; :: thesis: ( i in dom m & j = (p " ) . i implies m . i = (A @ ) * i,j )
assume A10: ( i in dom m & j = (p " ) . i ) ; :: thesis: m . i = (A @ ) * i,j
then A11: ((Path_matrix p,A) * (p " )) . i = (Path_matrix p,A) . ((p " ) . i) by A7, FUNCT_1:23;
A12: j in Seg n by A6, A7, A10, FUNCT_1:def 5;
then A13: j in dom (Path_matrix p,A) by A2, FINSEQ_1:def 3;
rng fp0 = Seg n by A5, FUNCT_2:def 3;
then i = p . j by A7, A8, A10, FUNCT_1:54;
then A14: (Path_matrix p,A) . j = A * j,i by A13, MATRIX_3:def 7;
A15: dom A = Seg (len A) by FINSEQ_1:def 3
.= Seg n by MATRIX_1:def 3 ;
len A = n by MATRIX_1:def 3;
then i in Seg (width A) by A1, A7, A8, A10, MATRIX_1:20;
then [j,i] in Indices A by A12, A15, ZFMISC_1:def 2;
hence m . i = (A @ ) * i,j by A10, A11, A14, MATRIX_1:def 7; :: thesis: verum

end;

hence Path_matrix (p " ),(A @ ) = (Path_matrix p,A) * (p " ) by A9, MATRIX_3:def 7; :: thesis: verum