let n be Nat; :: thesis:
let K be Field; :: thesis:
let i be Nat; :: thesis:
let M be Matrix of n,K; :: thesis:
assume A1: i in Seg n ; :: thesis:
reconsider N = n as Element of NAT by ORDINAL1:def 13;
reconsider X = finSeg N as non empty set by A1;
set P = Permutations n;
set Path = Path_product M;
set KK = the carrier of K;
set aa = the addF of K;
deffunc H₁( Element of Fin (Permutations n)) -> Element of the carrier of K = the addF of K $$ $1,(Path_product M);
consider g being Function of (Fin (Permutations n)),the carrier of K such that
A2: for x being Element of Fin (Permutations n) holds g . x = H₁(x) from FUNCT_2:sch 4();
deffunc H₂( set ) -> set = { p where p is Element of Permutations n : p . i = $1 } ;
consider f being Function such that
A3: ( dom f = X & ( for x being set st x in X holds
f . x = H₂(x) ) ) from FUNCT_1:sch 3();
rng f c= Fin (Permutations n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being set such that
A4: ( y in dom f & f . y = x ) by FUNCT_1:def 5;
X: Permutations n is finite by MATRIX_2:30;
H₂(y) c= Permutations n

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in H₂(y) ; :: thesis:
then ex p being Element of Permutations n st
( p = z & p . i = y ) ;
hence z in Permutations n ; :: thesis:

end;

then H₂(y) in Fin (Permutations n) by X, FINSUB_1:def 5;
hence x in Fin (Permutations n) by A3, A4; :: thesis:

end;

then reconsider f = f as Function of X,(Fin (Permutations n)) by A3, FUNCT_2:4;
set gf = g * f;
reconsider X' = X as Element of Fin X by FINSUB_1:def 5;

A6: now

let x, y be set ; :: thesis:
assume A7: ( x in X' & y in X' & f . x meets f . y ) ; :: thesis:
consider z being set such that
A8: ( z in f . x & z in f . y ) by A7, XBOOLE_0:3;
( f . x = H₂(x) & f . y = H₂(y) ) by A3, A7;
then ( ex p being Element of Permutations n st
( p = z & p . i = x ) & ex p being Element of Permutations n st
( p = z & p . i = y ) ) by A8;
hence x = y ; :: thesis:

end;

A9: for A, B being Element of Fin (Permutations n) st A misses B holds
the addF of K . (g . A),(g . B) = g . (A \/ B)

proof

let A, B be Element of Fin (Permutations n); :: thesis:
assume A10: A misses B ; :: thesis:
( g . (A \/ B) = H₁(A \/ B) & g . A = H₁(A) & g . B = H₁(B) & the addF of K is having_a_unity ) by A2, FVSUM_1:10;
hence the addF of K . (g . A),(g . B) = g . (A \/ B) by A10, SETWOP_2:6; :: thesis:

end;

A11: union (f .: X) c= Permutations n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union (f .: X) ; :: thesis:
then consider y being set such that
A12: ( x in y & y in f .: X ) by TARSKI:def 4;
consider z being set such that
A13: ( z in dom f & z in X & f . z = y ) by A12, FUNCT_1:def 12;
y = H₂(z) by A3, A13;
then ex p being Element of Permutations n st
( x = p & p . i = z ) by A12;
hence x in Permutations n ; :: thesis:

end;

Permutations n c= union (f .: X)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A14: x in Permutations n ; :: thesis:
then reconsider p = x as Permutation of X by MATRIX_2:def 11;
( dom p = X & rng p = X ) by FUNCT_2:67, FUNCT_2:def 3;
then p . i in X by A1, FUNCT_1:def 5;
then ( x in H₂(p . i) & f . (p . i) = H₂(p . i) & f . (p . i) in f .: X ) by A3, A14, FUNCT_1:def 12;
hence x in union (f .: X) by TARSKI:def 4; :: thesis:

end;

then A15: Permutations n = union (f .: X) by A11, XBOOLE_0:def 10;
set L = LaplaceExpL M,i;
set Laa = [#] (LaplaceExpL M,i),(the_unity_wrt the addF of K);
len (LaplaceExpL M,i) = n by Def7;
then A16: ( dom (LaplaceExpL M,i) = Seg n & dom (g * f) = X ) by FINSEQ_1:def 3, FUNCT_2:def 1;
then A17: ( dom (id X) = dom (LaplaceExpL M,i) & rng (id X) = X' & ([#] (LaplaceExpL M,i),(the_unity_wrt the addF of K)) | (dom (LaplaceExpL M,i)) = LaplaceExpL M,i & (g * f) * (id X) = g * f ) by RELAT_1:71, RELAT_1:78, SETWOP_2:23;

now

let x be set ; :: thesis:
assume A18: x in dom (g * f) ; :: thesis:
consider k being Element of NAT such that
A19: ( k = x & 1 <= k & k <= n ) by A16, A18;
( f . k in rng f & rng f c= Fin (Permutations n) ) by A3, A18, A19, FUNCT_1:def 5, RELAT_1:def 19;
then reconsider Fk = H₂(k) as Element of Fin (Permutations n) by A3, A18, A19;
( (g * f) . k = g . (f . k) & f . k = Fk ) by A3, A18, A19, FUNCT_1:23;
then ( (g * f) . k = H₁(Fk) & H₁(Fk) = (M * i,k) * (Cofactor M,i,k) ) by A1, A2, A18, A19, Th23;
hence (LaplaceExpL M,i) . x = (g * f) . x by A16, A18, A19, Def7; :: thesis:

end;

then A20: LaplaceExpL M,i = g * f by A16, FUNCT_1:9;
A21: ( the addF of K is having_a_unity & g . ({}. (Fin (Permutations n))) = the addF of K $$ ({}. (Permutations n)),(Path_product M) & Permutations n is finite ) by A2, FVSUM_1:10, MATRIX_2:30;
then ( g . {} = the_unity_wrt the addF of K & the addF of K is having_a_unity & FinOmega (Permutations n) = Permutations n ) by MATRIX_2:def 17, SETWISEO:40;
then ( the addF of K $$ X',(g * f) = the addF of K $$ (f .: X'),g & FinOmega X = X & the addF of K $$ (f .: X'),g = g . (FinOmega (Permutations n)) & g . (FinOmega (Permutations n)) = Det M ) by A2, A6, A9, A15, Th12, MATRIX_2:def 17;
hence Det M = the addF of K $$ (findom (LaplaceExpL M,i)),([#] (LaplaceExpL M,i),(the_unity_wrt the addF of K)) by A17, A20, SETWOP_2:7
.= Sum (LaplaceExpL M,i) by A21, SETWOP_2:def 2 ;
:: thesis: