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*> )
assume A1: 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*>
let p be Element of Permutations 3; :: thesis: ( p = <*2,3,1*> implies Path_matrix p,M = <*b,f,g*> )
assume A2: p = <*2,3,1*> ; :: thesis: Path_matrix p,M = <*b,f,g*>
A5: len (Path_matrix p,M) = 3 by MATRIX_3:def 7;
then A6: dom (Path_matrix p,M) = Seg 3 by FINSEQ_1:def 3;
then A7: 1 in dom (Path_matrix p,M) ;
A8: 2 = p . 1 by A2, FINSEQ_1:62;
A9: 2 in dom (Path_matrix p,M) by A6;
A10: 3 = p . 2 by A2, FINSEQ_1:62;
A11: 3 in dom (Path_matrix p,M) by A6;
A12: 1 = p . 3 by A2, FINSEQ_1:62;
A13: M . 1 = <*a,b,c*> by A1, FINSEQ_1:62;
[1,2] in Indices M by MATRIX_1:38;
then consider r being FinSequence of the carrier of K such that
A14: ( r = M . 1 & M * 1,2 = r . 2 ) by MATRIX_1:def 6;
r . 2 = b by A13, A14, FINSEQ_1:62;
then A15: (Path_matrix p,M) . 1 = b by A7, A8, A14, MATRIX_3:def 7;
A16: M . 2 = <*d,e,f*> by A1, FINSEQ_1:62;
[2,3] in Indices M by MATRIX_1:38;
then consider y being FinSequence of the carrier of K such that
A17: ( y = M . 2 & M * 2,3 = y . 3 ) by MATRIX_1:def 6;
y . 3 = f by A16, A17, FINSEQ_1:62;
then A18: (Path_matrix p,M) . 2 = f by A9, A10, A17, MATRIX_3:def 7;
A19: M . 3 = <*g,h,i*> by A1, FINSEQ_1:62;
[3,1] in Indices M by MATRIX_1:38;
then consider z being FinSequence of the carrier of K such that
A20: ( z = M . 3 & M * 3,1 = z . 1 ) by MATRIX_1:def 6;
z . 1 = g by A19, A20, FINSEQ_1:62;
then (Path_matrix p,M) . 3 = g by A11, A12, A20, MATRIX_3:def 7;
hence Path_matrix p,M = <*b,f,g*> by A5, A15, A18, FINSEQ_1:62; :: thesis: verum