let K be Field; :: thesis:
let n be Element of NAT ; :: thesis:
set B = FinOmega (Permutations n);
set f = Path_product (0. K,n,n);
set F = the addF of K;
set Y = the carrier of K;
set X = Permutations n;
reconsider G0 = (Fin (Permutations n)) --> (0. K) as Function of (Fin (Permutations n)),the carrier of K ;
A1: G0 . (FinOmega (Permutations n)) = 0. K by FUNCOP_1:13;
A2: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e

let e be Element of the carrier of K; :: thesis:
0. K is_a_unity_wrt the addF of K by FVSUM_1:8;
then A3: the addF of K . (0. K),e = e by BINOP_1:11;
assume e is_a_unity_wrt the addF of K ; :: thesis:
then the addF of K . (0. K),e = 0. K by BINOP_1:11;
hence G0 . {} = e by A3, FINSUB_1:18, FUNCOP_1:13; :: thesis:

end;

assume A4: n >= 1 ; :: thesis:
A5: for x being set st x in dom (Path_product (0. K,n,n)) holds
(Path_product (0. K,n,n)) . x = ((Permutations n) --> (0. K)) . x

let x be set ; :: thesis:
assume x in dom (Path_product (0. K,n,n)) ; :: thesis:
for p being Element of Permutations n holds ((Permutations n) --> (0. K)) . p = - (the multF of K $$ (Path_matrix p,(0. K,n,n))),p

defpred S₁[ Element of NAT ] means the multF of K $$ (($1 + 1) |-> (0. K)) = 0. K;
let p be Element of Permutations n; :: thesis:
A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
A7: ((k + 1) + 1) |-> (0. K) = ((k + 1) |-> (0. K)) ^ <*(0. K)*> by FINSEQ_2:74;
assume S₁[k] ; :: thesis:
then the multF of K $$ (((k + 1) + 1) |-> (0. K)) = (0. K) * (0. K) by A7, FINSOP_1:5, FVSUM_1:11
.= 0. K by VECTSP_1:36 ;
hence S₁[k + 1] ; :: thesis:

end;

1 |-> (0. K) = <*(0. K)*> by FINSEQ_2:73;
then A8: S₁[ 0 ] by FINSOP_1:12;
A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A6);

A10: now

case p is even ; :: thesis:

hence - (0. K),p = 0. K by MATRIX_2:def 16; :: thesis:

end;

case not p is even ; :: thesis:

then - (0. K),p = - (0. K) by MATRIX_2:def 16
.= 0. K by RLVECT_1:25 ;
hence - (0. K),p = 0. K ; :: thesis:

end;

end;

end;

A11: for i, j being Nat st i in dom (n |-> (0. K)) & j = p . i holds
(n |-> (0. K)) . i = (0. K,n,n) * i,j

let i, j be Nat; :: thesis:
assume that
A12: i in dom (n |-> (0. K)) and
A13: j = p . i ; :: thesis:
A14: i in Seg n by A12, FUNCOP_1:19;
then j in Seg n by A13, Th14;
then A15: j in Seg (width (0. K,n,n)) by A4, MATRIX_1:24;
i in dom (0. K,n,n) by A14, Th13;
then A16: [i,j] in Indices (0. K,n,n) by A15, ZFMISC_1:def 2;
(n |-> (0. K)) . i = 0. K by A14, FUNCOP_1:13;
hence (n |-> (0. K)) . i = (0. K,n,n) * i,j by A16, MATRIX_3:3; :: thesis:

end;

len (n |-> (0. K)) = n by FINSEQ_1:def 18;
then A17: Path_matrix p,(0. K,n,n) = n |-> (0. K) by A11, MATRIX_3:def 7;
n -' 1 = n - 1 by A4, XREAL_1:235;
then A18: (n -' 1) + 1 = n ;
((Permutations n) --> (0. K)) . p = 0. K by FUNCOP_1:13;
hence ((Permutations n) --> (0. K)) . p = - (the multF of K $$ (Path_matrix p,(0. K,n,n))),p by A17, A9, A18, A10; :: thesis:

end;

hence (Path_product (0. K,n,n)) . x = ((Permutations n) --> (0. K)) . x by MATRIX_3:def 8; :: thesis:

end;

dom ((Permutations n) --> (0. K)) = Permutations n by FUNCOP_1:19;
then dom (Path_product (0. K,n,n)) = dom ((Permutations n) --> (0. K)) by FUNCT_2:def 1;
then A19: Path_product (0. K,n,n) = (Permutations n) --> (0. K) by A5, FUNCT_1:9;
A20: for x being Element of Permutations n holds G0 . {x} = (Path_product (0. K,n,n)) . x

let x be Element of Permutations n; :: thesis:
G0 . {.x.} = 0. K by FUNCOP_1:13;
hence G0 . {x} = (Path_product (0. K,n,n)) . x by A19, FUNCOP_1:13; :: thesis:

end;

A21: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (0. K,n,n)) . x)

let B9 be Element of Fin (Permutations n); :: thesis:
assume that
B9 c= FinOmega (Permutations n) and
B9 <> {} ; :: thesis:
thus for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (0. K,n,n)) . x) :: thesis:

let x be Element of Permutations n; :: thesis:
assume x in (FinOmega (Permutations n)) \ B9 ; :: thesis:
A22: ( G0 . (B9 \/ {.x.}) = 0. K & G0 . B9 = 0. K ) by FUNCOP_1:13;
( (Path_product (0. K,n,n)) . x = 0. K & 0. K is_a_unity_wrt the addF of K ) by A19, FUNCOP_1:13, FVSUM_1:8;
hence G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (0. K,n,n)) . x) by A22, BINOP_1:11; :: thesis:

end;

end;

( FinOmega (Permutations n) <> {} or the addF of K is having_a_unity ) by MATRIX_2:30, MATRIX_2:def 17;
then the addF of K $$ (FinOmega (Permutations n)),(Path_product (0. K,n,n)) = 0. K by A1, A2, A20, A21, SETWISEO:def 3;
hence Det (0. K,n,n) = 0. K by MATRIX_3:def 9; :: thesis: