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

Path_matrix (p,M) = <*b,d,i*>

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

Path_matrix (p,M) = <*b,d,i*>

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

Path_matrix (p,M) = <*b,d,i*> )

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

Path_matrix (p,M) = <*b,d,i*>

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

then A4: r . 2 = b by A1, FINSEQ_1:45;

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

M . 3 = <*g,h,i*> by A3, FINSEQ_1:45;

then A7: z . 3 = i by A5, FINSEQ_1:45;

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

then A10: y . 1 = d by A8, FINSEQ_1:45;

let p be Element of Permutations 3; :: thesis: ( p = <*2,1,3*> implies Path_matrix (p,M) = <*b,d,i*> )

assume A11: p = <*2,1,3*> ; :: thesis: Path_matrix (p,M) = <*b,d,i*>

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

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

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

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

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

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

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

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

Path_matrix (p,M) = <*b,d,i*>

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

Path_matrix (p,M) = <*b,d,i*>

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

Path_matrix (p,M) = <*b,d,i*> )

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

Path_matrix (p,M) = <*b,d,i*>

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

then A4: r . 2 = b by A1, FINSEQ_1:45;

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

M . 3 = <*g,h,i*> by A3, FINSEQ_1:45;

then A7: z . 3 = i by A5, FINSEQ_1:45;

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

then A10: y . 1 = d by A8, FINSEQ_1:45;

let p be Element of Permutations 3; :: thesis: ( p = <*2,1,3*> implies Path_matrix (p,M) = <*b,d,i*> )

assume A11: p = <*2,1,3*> ; :: thesis: Path_matrix (p,M) = <*b,d,i*>

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

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

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

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

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

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

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

hence Path_matrix (p,M) = <*b,d,i*> by A15, A17, A18, FINSEQ_1:45; :: thesis: verum