let K be Field; :: thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*>

let a, b, c, d, e, f, g, h, i be Element of K; :: thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*>

let M be Matrix of 3,K; :: thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*> )

[1,3] in Indices M by MATRIX_0:31;
then consider r being FinSequence of the carrier of K such that
A1: r = M . 1 and
A2: M * (1,3) = r . 3 by MATRIX_0:def 5;
assume A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*>

then M . 1 = <*a,b,c*> by FINSEQ_1:45;
then A4: r . 3 = c by ;
[3,2] in Indices M by MATRIX_0:31;
then consider z being FinSequence of the carrier of K such that
A5: z = M . 3 and
A6: M * (3,2) = z . 2 by MATRIX_0:def 5;
M . 3 = <*g,h,i*> by ;
then A7: z . 2 = h by ;
[2,1] in Indices M by MATRIX_0:31;
then consider y being FinSequence of the carrier of K such that
A8: y = M . 2 and
A9: M * (2,1) = y . 1 by MATRIX_0:def 5;
M . 2 = <*d,e,f*> by ;
then A10: y . 1 = d by ;
let p be Element of Permutations 3; :: thesis: ( p = <*3,1,2*> implies Path_matrix (p,M) = <*c,d,h*> )
assume A11: p = <*3,1,2*> ; :: thesis: Path_matrix (p,M) = <*c,d,h*>
then A12: 3 = p . 1 by FINSEQ_1:45;
A13: 2 = p . 3 by ;
A14: 1 = p . 2 by ;
A15: len (Path_matrix (p,M)) = 3 by MATRIX_3:def 7;
then A16: dom (Path_matrix (p,M)) = Seg 3 by FINSEQ_1:def 3;
then 2 in dom (Path_matrix (p,M)) ;
then A17: (Path_matrix (p,M)) . 2 = d by ;
3 in dom (Path_matrix (p,M)) by A16;
then A18: (Path_matrix (p,M)) . 3 = h by ;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = c by ;
hence Path_matrix (p,M) = <*c,d,h*> by ; :: thesis: verum