let K be Field; :: thesis:
let n be Element of NAT ; :: thesis:
set B = In ((Permutations n),(Fin (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

let e be Element of the carrier of K; :: thesis:
0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
then A2: the addF of K . ((0. K),e) = e by BINOP_1:3;
assume e is_a_unity_wrt the addF of K ; :: thesis:
then the addF of K . ((0. K),e) = 0. K by BINOP_1:3;
hence G0 . {} = e by A2, FINSUB_1:7, FUNCOP_1:7; :: thesis:

end;

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

let x be object ; :: thesis:
assume x in dom (PPath_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))))

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

let k be Nat; :: thesis:
A6: ((k + 1) + 1) |-> (0. K) = ((k + 1) |-> (0. K)) ^ <*(0. K)*> by FINSEQ_2:60;
assume S₁[k] ; :: thesis:
then the multF of K $$ (((k + 1) + 1) |-> (0. K)) = (0. K) * (0. K) by A6, FINSOP_1:4
.= 0. K ;
hence S₁[k + 1] ; :: thesis:

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)

let i, j be Nat; :: thesis:
assume that
A8: i in dom (n |-> (0. K)) and
A9: j = p . i ; :: thesis:
A10: i in Seg n by A8, FUNCOP_1:13;
then j in Seg n by A9, MATRIX_7:14;
then A11: j in Seg (width (0. (K,n,n))) by A3, MATRIX_0:23;
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_0:def 4;
(n |-> (0. K)) . i = 0. K by A10, FUNCOP_1:7;
hence (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) by A12, MATRIX_3:1; :: thesis:

end;

len (n |-> (0. K)) = n by CARD_1:def 7;
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:235;
1 |-> (0. K) = <*(0. K)*> by FINSEQ_2:59;
then A15: S₁[ 0 ] by FINSOP_1:11;
for k being Nat holds S₁[k] from NAT_1:sch 2(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:7; :: thesis:

end;

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

end;

dom ((Permutations n) --> (0. K)) = Permutations n by FUNCOP_1:13;
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:2;
A17: for x being Element of Permutations n holds G0 . {x} = (PPath_product (0. (K,n,n))) . x

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

end;

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

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

let x be Element of Permutations n; :: thesis:
assume x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 ; :: thesis:
A19: ( G0 . (B9 \/ {.x.}) = 0. K & G0 . B9 = 0. K ) by FUNCOP_1:7;
( (PPath_product (0. (K,n,n))) . x = 0. K & 0. K is_a_unity_wrt the addF of K ) by A16, FUNCOP_1:7, FVSUM_1:6;
hence G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) by A19, BINOP_1:3; :: thesis:

end;

end;

Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;
then ( In ((Permutations n),(Fin (Permutations n))) <> {} & G0 . (In ((Permutations n),(Fin (Permutations n)))) = 0. K ) by FUNCOP_1:7;
hence Per (0. (K,n,n)) = 0. K by A1, A17, A18, SETWISEO:def 3; :: thesis: