let K be Field; :: thesis: for n being Element of NAT st n >= 1 holds
Per (0. K,n,n) = 0. K
let n be Element of NAT ; :: thesis: ( n >= 1 implies Per (0. K,n,n) = 0. K )
set B = FinOmega (Permutations n);
set f = PPath_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: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e

proof

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

end;

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

proof

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

proof

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

proof

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

end;

A7: 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

proof

let i, j be Nat; :: thesis: ( i in dom (n |-> (0. K)) & j = p . i implies (n |-> (0. K)) . i = (0. K,n,n) * i,j )
assume that
A8: i in dom (n |-> (0. K)) and
A9: j = p . i ; :: thesis: (n |-> (0. K)) . i = (0. K,n,n) * i,j
A10: i in Seg n by A8, FUNCOP_1:19;
then j in Seg n by A9, MATRIX_7:14;
then A11: j in Seg (width (0. K,n,n)) by A3, MATRIX_1:24;
i in dom (0. K,n,n) by A10, MATRIX_7:13;
then [i,j] in [:(dom (0. K,n,n)),(Seg (width (0. K,n,n))):] by A11, ZFMISC_1:def 2;
then A12: [i,j] in Indices (0. K,n,n) by MATRIX_1:def 5;
(n |-> (0. K)) . i = 0. K by A10, FUNCOP_1:13;
hence (n |-> (0. K)) . i = (0. K,n,n) * i,j by A12, MATRIX_3:3; :: thesis: verum

end;

len (n |-> (0. K)) = n by FINSEQ_1:def 18;
then A13: Path_matrix p,(0. K,n,n) = n |-> (0. K) by A7, MATRIX_3:def 7;
A14: (n -' 1) + 1 = n by A3, XREAL_1:237;
1 |-> (0. K) = <*(0. K)*> by FINSEQ_2:73;
then A15: S₁[ 0 ] by FINSOP_1:12;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A15, A5);
then the multF of K $$ (Path_matrix p,(0. K,n,n)) = 0. K by A13, A14;
hence ((Permutations n) --> (0. K)) . p = the multF of K $$ (Path_matrix p,(0. K,n,n)) by FUNCOP_1:13; :: thesis: verum

end;

hence (PPath_product (0. K,n,n)) . x = ((Permutations n) --> (0. K)) . x by Def1; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

proof

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

end;

end;

( FinOmega (Permutations n) <> {} & G0 . (FinOmega (Permutations n)) = 0. K ) by FUNCOP_1:13, MATRIX_2:30, MATRIX_2:def 17;
hence Per (0. K,n,n) = 0. K by A1, A17, A18, SETWISEO:def 3; :: thesis: verum