let K be Field; :: thesis: for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = Rev () holds
Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*>

let a, b, c, d be Element of K; :: thesis: for p being Element of Permutations 2 st p = Rev () holds
Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*>

let p be Element of Permutations 2; :: thesis: ( p = Rev () implies Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*> )
assume A1: p = Rev () ; :: thesis: Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*>
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 1 in dom (Path_matrix (p,((a,b) ][ (c,d)))) ;
then A4: (Path_matrix (p,((a,b) ][ (c,d)))) . 1 = ((a,b) ][ (c,d)) * (1,2) by
.= b by MATRIX_0:50 ;
2 in dom (Path_matrix (p,((a,b) ][ (c,d)))) by A3;
then (Path_matrix (p,((a,b) ][ (c,d)))) . 2 = ((a,b) ][ (c,d)) * (2,1) by
.= c by MATRIX_0:50 ;
hence Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*> by ; :: thesis: verum