let K be Field; :: thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)

reconsider a3 = <*1,3,2*>, a4 = <*2,3,1*>, a5 = <*2,1,3*>, a6 = <*3,1,2*> as Element of Permutations 3 by Th27;
reconsider id3 = idseq 3 as Permutation of (Seg 3) ;
reconsider Id3 = idseq 3 as Element of Permutations 3 by MATRIX_1:def 12;
A1: id3 is even by MATRIX_1:16;
reconsider rid3 = Rev () as Element of Permutations 3 by Th4;
let a, b, c, d, e, f, g, h, i be Element of K; :: thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)

let M be Matrix of 3,K; :: thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) )
assume A2: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
Permutations 3 in Fin () by FINSUB_1:def 5;
then In ((),(Fin ())) = Permutations 3 by SUBSET_1:def 8;
then reconsider X = {Id3,rid3,a3,a4,a5,a6} as Element of Fin () by ;
reconsider B1 = {.Id3,rid3,a3.}, B2 = {.a4,a5,a6.} as Element of Fin () ;
set F = the addF of K;
A3: ( In ((),(Fin ())) = X & X = {Id3,rid3,a3} \/ {a4,a5,a6} ) by ;
now :: thesis: for x being object st x in B1 holds
x in B1 \ B2
let x be object ; :: thesis: ( x in B1 implies x in B1 \ B2 )
assume A4: x in B1 ; :: thesis: x in B1 \ B2
then ( x = Id3 or x = rid3 or x = a3 ) by ENUMSET1:def 1;
then not x in B2 by ;
hence x in B1 \ B2 by ; :: thesis: verum
end;
then A5: B1 c= B1 \ B2 by TARSKI:def 3;
for x being object st x in B1 \ B2 holds
x in B1 by XBOOLE_0:def 5;
then B1 \ B2 c= B1 by TARSKI:def 3;
then B1 \ B2 = B1 by ;
then A6: B1 misses B2 by XBOOLE_1:83;
set r = Path_product M;
A7: 3 = len () by MATRIX_1:9;
then Id3 is even by MATRIX_1:16;
then reconsider r1 = () . id3, r2 = () . rid3, r3 = () . a3, r4 = () . a4, r5 = () . a5, r6 = () . a6 as Element of K by FUNCT_2:5;
A8: () . id3 = - (( the multF of K \$\$ (Path_matrix (Id3,M))),Id3) by MATRIX_3:def 8
.= the multF of K \$\$ (Path_matrix (Id3,M)) by
.= the multF of K \$\$ <*a,e,i*> by
.= (a * e) * i by Th26 ;
A9: () . a6 = - (( the multF of K \$\$ (Path_matrix (a6,M))),a6) by MATRIX_3:def 8
.= the multF of K \$\$ (Path_matrix (a6,M)) by
.= the multF of K \$\$ <*c,d,h*> by
.= (c * d) * h by Th26 ;
A10: () . a5 = - (( the multF of K \$\$ (Path_matrix (a5,M))),a5) by MATRIX_3:def 8
.= - ( the multF of K \$\$ (Path_matrix (a5,M))) by
.= - ( the multF of K \$\$ <*b,d,i*>) by
.= - ((b * d) * i) by Th26 ;
A11: () . a4 = - (( the multF of K \$\$ (Path_matrix (a4,M))),a4) by MATRIX_3:def 8
.= the multF of K \$\$ (Path_matrix (a4,M)) by
.= the multF of K \$\$ <*b,f,g*> by
.= (b * f) * g by Th26 ;
A12: () . a3 = - (( the multF of K \$\$ (Path_matrix (a3,M))),a3) by MATRIX_3:def 8
.= - ( the multF of K \$\$ (Path_matrix (a3,M))) by
.= - ( the multF of K \$\$ <*a,f,h*>) by
.= - ((a * f) * h) by Th26 ;
A13: () . rid3 = - (( the multF of K \$\$ (Path_matrix (rid3,M))),rid3) by MATRIX_3:def 8
.= - ( the multF of K \$\$ (Path_matrix (rid3,M))) by
.= - ( the multF of K \$\$ <*c,e,g*>) by
.= - ((c * e) * g) by Th26 ;
A14: ( the addF of K \$\$ (B1,()) = (r1 + r2) + r3 & the addF of K \$\$ (B2,()) = (r4 + r5) + r6 ) by ;
Det M = the addF of K \$\$ ((In ((),(Fin ()))),()) by MATRIX_3:def 9
.= the addF of K . (( the addF of K \$\$ (B1,())),( the addF of K \$\$ (B2,()))) by
.= ((r1 + r2) + r3) + (r4 + (r5 + r6)) by
.= (((r1 + r2) + r3) + r4) + (r5 + r6) by RLVECT_1:def 3
.= ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) by ;
hence Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) ; :: thesis: verum