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 = In ((),(Fin ()));
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 ()) --> (0. K) as Function of (Fin ()), 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: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: G0 . {} = e
then the addF of K . ((0. K),e) = 0. K by BINOP_1:3;
hence G0 . {} = e by ; :: thesis: verum
end;
assume A3: n >= 1 ; :: thesis: Per (0. (K,n,n)) = 0. K
A4: for x being object st x in dom (PPath_product (0. (K,n,n))) holds
(PPath_product (0. (K,n,n))) . x = (() --> (0. K)) . x
proof
let x be object ; :: thesis: ( x in dom (PPath_product (0. (K,n,n))) implies (PPath_product (0. (K,n,n))) . x = (() --> (0. K)) . x )
assume x in dom (PPath_product (0. (K,n,n))) ; :: thesis: (PPath_product (0. (K,n,n))) . x = (() --> (0. K)) . x
for p being Element of Permutations n holds (() --> (0. K)) . p = the multF of K \$\$ (Path_matrix (p,(0. (K,n,n))))
proof
defpred S1[ Nat] means the multF of K \$\$ ((\$1 + 1) |-> (0. K)) = 0. K;
let p be Element of Permutations n; :: thesis: (() --> (0. K)) . p = the multF of K \$\$ (Path_matrix (p,(0. (K,n,n))))
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A6: ((k + 1) + 1) |-> (0. K) = ((k + 1) |-> (0. K)) ^ <*(0. K)*> by FINSEQ_2:60;
assume S1[k] ; :: thesis: S1[k + 1]
then the multF of K \$\$ (((k + 1) + 1) |-> (0. K)) = (0. K) * (0. K) by
.= 0. K ;
hence S1[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 ;
then j in Seg n by ;
then A11: j in Seg (width (0. (K,n,n))) by ;
i in dom (0. (K,n,n)) by ;
then [i,j] in [:(dom (0. (K,n,n))),(Seg (width (0. (K,n,n)))):] by ;
then A12: [i,j] in Indices (0. (K,n,n)) by MATRIX_0:def 4;
(n |-> (0. K)) . i = 0. K by ;
hence (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) by ; :: thesis: verum
end;
len (n |-> (0. K)) = n by CARD_1:def 7;
then A13: Path_matrix (p,(0. (K,n,n))) = n |-> (0. K) by ;
A14: (n -' 1) + 1 = n by ;
1 |-> (0. K) = <*(0. K)*> by FINSEQ_2:59;
then A15: S1[ 0 ] by FINSOP_1:11;
for k being Nat holds S1[k] from NAT_1:sch 2(A15, A5);
then the multF of K \$\$ (Path_matrix (p,(0. (K,n,n)))) = 0. K by ;
hence ((Permutations n) --> (0. K)) . p = the multF of K \$\$ (Path_matrix (p,(0. (K,n,n)))) by FUNCOP_1:7; :: thesis: verum
end;
hence (PPath_product (0. (K,n,n))) . x = (() --> (0. K)) . x by Def1; :: thesis: verum
end;
dom (() --> (0. K)) = Permutations n by FUNCOP_1:13;
then dom (PPath_product (0. (K,n,n))) = dom (() --> (0. K)) by FUNCT_2:def 1;
then A16: PPath_product (0. (K,n,n)) = () --> (0. K) by ;
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:7;
hence G0 . {x} = (PPath_product (0. (K,n,n))) . x by ; :: thesis: verum
end;
A18: for B9 being Element of Fin () st B9 c= In ((),(Fin ())) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((),(Fin ()))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x))
proof
let B9 be Element of Fin (); :: thesis: ( B9 c= In ((),(Fin ())) & B9 <> {} implies for x being Element of Permutations n st x in (In ((),(Fin ()))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) )

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

thus for x being Element of Permutations n st x in (In ((),(Fin ()))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) :: thesis: verum
proof
let x be Element of Permutations n; :: thesis: ( x in (In ((),(Fin ()))) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) )
assume x in (In ((),(Fin ()))) \ B9 ; :: thesis: G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x))
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 ;
hence G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) by ; :: thesis: verum
end;
end;
Permutations n in Fin () by FINSUB_1:def 5;
then In ((),(Fin ())) = Permutations n by SUBSET_1:def 8;
then ( In ((),(Fin ())) <> {} & G0 . (In ((),(Fin ()))) = 0. K ) by FUNCOP_1:7;
hence Per (0. (K,n,n)) = 0. K by ; :: thesis: verum