let K be Field; :: thesis: for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix p,(a,b ][ c,d) = <*a,d*>
let a, b, c, d be Element of K; :: thesis: for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix p,(a,b ][ c,d) = <*a,d*>
let p be Element of Permutations 2; :: thesis: ( p = idseq 2 implies Path_matrix p,(a,b ][ c,d) = <*a,d*> )
assume A1: p = idseq 2 ; :: thesis: Path_matrix p,(a,b ][ c,d) = <*a,d*>
A2: len (Path_matrix p,(a,b ][ c,d)) = 2 by MATRIX_3:def 7;
then A3: dom (Path_matrix p,(a,b ][ c,d)) = Seg 2 by FINSEQ_1:def 3;
then A4: 2 in dom (Path_matrix p,(a,b ][ c,d)) ;
then 2 = p . 2 by A1, A3, FUNCT_1:35;
then A5: (Path_matrix p,(a,b ][ c,d)) . 2 = (a,b ][ c,d) * 2,2 by A4, MATRIX_3:def 7
.= d by MATRIX_2:6 ;
A6: 1 in dom (Path_matrix p,(a,b ][ c,d)) by A3;
then 1 = p . 1 by A1, A3, FUNCT_1:35;
then (Path_matrix p,(a,b ][ c,d)) . 1 = (a,b ][ c,d) * 1,1 by A6, MATRIX_3:def 7
.= a by MATRIX_2:6 ;
hence Path_matrix p,(a,b ][ c,d) = <*a,d*> by A2, A5, FINSEQ_1:61; :: thesis: verum