let n be Nat; :: thesis: for K being commutative Ring
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 commutative Ring; :: 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 ") )
set f = Path_matrix (p,A);
reconsider fp = p " as Function of (Seg n),(Seg n) by MATRIX_1:def 12;
reconsider fp0 = p as Function of (Seg n),(Seg n) by MATRIX_1:def 12;
assume A1: n >= 1 ; :: thesis: Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
then A2: dom fp = Seg n by FUNCT_2:def 1;
A3: len (Path_matrix (p,A)) = n by MATRIX_3:def 7;
then reconsider m = (Path_matrix (p,A)) * (p ") as FinSequence of K by A1, Th33;
p " is Permutation of (Seg n) by MATRIX_1:def 12;
then A4: rng fp = Seg n by FUNCT_2:def 3;
then rng (p ") c= dom (Path_matrix (p,A)) by A3, FINSEQ_1:def 3;
then A5: dom ((Path_matrix (p,A)) * (p ")) = dom fp by RELAT_1:27;
A6: p is Permutation of (Seg n) by MATRIX_1:def 12;
A7: 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 that
A8: i in dom m and
A9: j = (p ") . i ; :: thesis: m . i = (A @) * (i,j)
A10: j in Seg n by A4, A5, A8, A9, FUNCT_1:def 3;
then A11: j in dom (Path_matrix (p,A)) by A3, FINSEQ_1:def 3;
rng fp0 = Seg n by A6, FUNCT_2:def 3;
then i = p . j by A5, A2, A8, A9, FUNCT_1:32;
then A12: (Path_matrix (p,A)) . j = A * (j,i) by A11, MATRIX_3:def 7;
A13: dom A = Seg (len A) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:def 2 ;
len A = n by MATRIX_0:def 2;
then i in Seg (width A) by A1, A5, A2, A8, MATRIX_0:20;
then A14: [j,i] in Indices A by A10, A13, ZFMISC_1:def 2;
((Path_matrix (p,A)) * (p ")) . i = (Path_matrix (p,A)) . ((p ") . i) by A5, A8, FUNCT_1:13;
hence m . i = (A @) * (i,j) by A9, A12, A14, MATRIX_0:def 6; :: thesis: verum

end;

n in NAT by ORDINAL1:def 12;
then len m = n by A5, A2, FINSEQ_1:def 3;
hence Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ") by A7, MATRIX_3:def 7; :: thesis: verum