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 = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*>

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 = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*>

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 = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*> )

[1,2] 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,2) = r . 2 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 = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*>

then M . 1 = <*a,b,c*> by FINSEQ_1:45;
then A4: r . 2 = b by ;
[3,1] 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,1) = z . 1 by MATRIX_0:def 5;
M . 3 = <*g,h,i*> by ;
then A7: z . 1 = g by ;
[2,3] 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,3) = y . 3 by MATRIX_0:def 5;
M . 2 = <*d,e,f*> by ;
then A10: y . 3 = f by ;
let p be Element of Permutations 3; :: thesis: ( p = <*2,3,1*> implies Path_matrix (p,M) = <*b,f,g*> )
assume A11: p = <*2,3,1*> ; :: thesis: Path_matrix (p,M) = <*b,f,g*>
then A12: 2 = p . 1 by FINSEQ_1:45;
A13: 1 = p . 3 by ;
A14: 3 = 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 = f by ;
3 in dom (Path_matrix (p,M)) by A16;
then A18: (Path_matrix (p,M)) . 3 = g by ;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = b by ;
hence Path_matrix (p,M) = <*b,f,g*> by ; :: thesis: verum