let K be Field; 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; Per (a,b ][ c,d) = (a * d) + (b * c)
reconsider rid2 = Rev (idseq 2) as Element of Permutations 2 by Th4;
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) ;
set f = PPath_product (a,b ][ c,d);
1 in Seg 2
;
then A1:
( FinOmega (Permutations 2) = Permutations 2 & id2 <> rid2 )
by Th2, FUNCT_1:35, MATRIX_2:30, MATRIX_2:def 17;
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
;
(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
;
hence
Per (a,b ][ c,d) = (a * d) + (b * c)
by A2, A1, Th6, SETWOP_2:3; verum