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,2,1*> holds

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

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

Path_matrix (p,M) = <*c,e,g*> )

[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,2,1*> holds

Path_matrix (p,M) = <*c,e,g*>

then M . 1 = <*a,b,c*> by FINSEQ_1:45;

then A4: r . 3 = c by A1, FINSEQ_1:45;

[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 A3, FINSEQ_1:45;

then A7: z . 1 = g by A5, FINSEQ_1:45;

[2,2] 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,2) = y . 2 by MATRIX_0:def 5;

M . 2 = <*d,e,f*> by A3, FINSEQ_1:45;

then A10: y . 2 = e by A8, FINSEQ_1:45;

let p be Element of Permutations 3; :: thesis: ( p = <*3,2,1*> implies Path_matrix (p,M) = <*c,e,g*> )

assume A11: p = <*3,2,1*> ; :: thesis: Path_matrix (p,M) = <*c,e,g*>

then A12: 3 = p . 1 by FINSEQ_1:45;

A13: 1 = p . 3 by A11, FINSEQ_1:45;

A14: 2 = p . 2 by A11, FINSEQ_1:45;

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 = e by A14, A9, A10, MATRIX_3:def 7;

3 in dom (Path_matrix (p,M)) by A16;

then A18: (Path_matrix (p,M)) . 3 = g by A13, A6, A7, MATRIX_3:def 7;

1 in dom (Path_matrix (p,M)) by A16;

then (Path_matrix (p,M)) . 1 = c by A12, A2, A4, MATRIX_3:def 7;

hence Path_matrix (p,M) = <*c,e,g*> by A15, A17, A18, FINSEQ_1:45; :: thesis: verum

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,2,1*> holds

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

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

Path_matrix (p,M) = <*c,e,g*> )

[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,2,1*> holds

Path_matrix (p,M) = <*c,e,g*>

then M . 1 = <*a,b,c*> by FINSEQ_1:45;

then A4: r . 3 = c by A1, FINSEQ_1:45;

[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 A3, FINSEQ_1:45;

then A7: z . 1 = g by A5, FINSEQ_1:45;

[2,2] 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,2) = y . 2 by MATRIX_0:def 5;

M . 2 = <*d,e,f*> by A3, FINSEQ_1:45;

then A10: y . 2 = e by A8, FINSEQ_1:45;

let p be Element of Permutations 3; :: thesis: ( p = <*3,2,1*> implies Path_matrix (p,M) = <*c,e,g*> )

assume A11: p = <*3,2,1*> ; :: thesis: Path_matrix (p,M) = <*c,e,g*>

then A12: 3 = p . 1 by FINSEQ_1:45;

A13: 1 = p . 3 by A11, FINSEQ_1:45;

A14: 2 = p . 2 by A11, FINSEQ_1:45;

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 = e by A14, A9, A10, MATRIX_3:def 7;

3 in dom (Path_matrix (p,M)) by A16;

then A18: (Path_matrix (p,M)) . 3 = g by A13, A6, A7, MATRIX_3:def 7;

1 in dom (Path_matrix (p,M)) by A16;

then (Path_matrix (p,M)) . 1 = c by A12, A2, A4, MATRIX_3:def 7;

hence Path_matrix (p,M) = <*c,e,g*> by A15, A17, A18, FINSEQ_1:45; :: thesis: verum