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 = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,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 = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,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 = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,i*> )
[1,1] 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,1) = r . 1 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 = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,i*>
then M . 1 = <*a,b,c*> ;
then A4: r . 1 = a by A1;
[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;
then A7: z . 3 = i by A5;
[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;
then A10: y . 2 = e by A8;
let p be Element of Permutations 3; :: thesis: ( p = <*1,2,3*> implies Path_matrix (p,M) = <*a,e,i*> )
assume A11: p = <*1,2,3*> ; :: thesis: Path_matrix (p,M) = <*a,e,i*>
then A12: 1 = p . 1 ;
A13: 3 = p . 3 by A11;
A14: 2 = p . 2 by A11;
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 = i by A13, A6, A7, MATRIX_3:def 7;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = a by A12, A2, A4, MATRIX_3:def 7;
hence Path_matrix (p,M) = <*a,e,i*> by A15, A17, A18, FINSEQ_1:45; :: thesis: verum