let K be Field; :: thesis: for a, b, c, d being Element of K holds Per (a,b ][ c,d) = (a * d) + (b * c)
let a, b, c, d be Element of K; :: thesis: Per (a,b ][ c,d) = (a * d) + (b * c)
set M = a,b ][ c,d;
reconsider Id2 = idseq 2 as Element of Permutations 2 by MATRIX_2:def 11;
reconsider id2 = Id2 as Permutation of (Seg 2) ;
reconsider rid2 = Rev (idseq 2) as Element of Permutations 2 by Th4;
set f = PPath_product (a,b ][ c,d);
A1: (PPath_product (a,b ][ c,d)) . id2 = the multF of K $$ (Path_matrix Id2,(a,b ][ c,d)) by Def1
.= the multF of K $$ <*a,d*> by Th9
.= a * d by Th11 ;
A2: (PPath_product (a,b ][ c,d)) . rid2 = the multF of K $$ (Path_matrix rid2,(a,b ][ c,d)) by Def1
.= the multF of K $$ <*b,c*> by Th10
.= b * c by Th11 ;
A3: FinOmega (Permutations 2) = Permutations 2 by MATRIX_2:30, MATRIX_2:def 17;
1 in Seg 2 ;
then id2 <> rid2 by Th2, FUNCT_1:35;
hence Per (a,b ][ c,d) = (a * d) + (b * c) by A1, A2, A3, Th6, SETWOP_2:3; :: thesis: verum