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:18;

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_0:50 ;

A6: 1 in dom (Path_matrix (p,((a,b) ][ (c,d)))) by A3;

then 1 = p . 1 by A1, A3, FUNCT_1:18;

then (Path_matrix (p,((a,b) ][ (c,d)))) . 1 = ((a,b) ][ (c,d)) * (1,1) by A6, MATRIX_3:def 7

.= a by MATRIX_0:50 ;

hence Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*> by A2, A5, FINSEQ_1:44; :: thesis: verum

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:18;

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_0:50 ;

A6: 1 in dom (Path_matrix (p,((a,b) ][ (c,d)))) by A3;

then 1 = p . 1 by A1, A3, FUNCT_1:18;

then (Path_matrix (p,((a,b) ][ (c,d)))) . 1 = ((a,b) ][ (c,d)) * (1,1) by A6, MATRIX_3:def 7

.= a by MATRIX_0:50 ;

hence Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*> by A2, A5, FINSEQ_1:44; :: thesis: verum