let K be Field; 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; 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; ( 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*>*>
; 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; ( p = <*3,2,1*> implies Path_matrix (p,M) = <*c,e,g*> )
assume A11:
p = <*3,2,1*>
; 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; verum