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 ((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

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

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

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))

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

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 ((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

proof

assume A3:
n >= 1
; :: thesis: Per (0. (K,n,n)) = 0. K
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 A2, FINSUB_1:7, FUNCOP_1:7; :: thesis: verum

end;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 A2, FINSUB_1:7, FUNCOP_1:7; :: thesis: verum

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

proof

dom ((Permutations n) --> (0. K)) = Permutations n
by FUNCOP_1:13;
let x be object ; :: 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))))

end;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

hence
(PPath_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x
by Def1; :: thesis: verum
defpred S_{1}[ 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 Nat st S_{1}[k] holds

S_{1}[k + 1]

(n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)

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_{1}[ 0 ]
by FINSOP_1:11;

for k being Nat holds S_{1}[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: verum

end;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 Nat st S

S

proof

A7:
for i, j being Nat st i in dom (n |-> (0. K)) & j = p . i holds
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

A6: ((k + 1) + 1) |-> (0. K) = ((k + 1) |-> (0. K)) ^ <*(0. K)*> by FINSEQ_2:60;

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then the multF of K $$ (((k + 1) + 1) |-> (0. K)) = (0. K) * (0. K) by A6, FINSOP_1:4

.= 0. K ;

hence S_{1}[k + 1]
; :: thesis: verum

end;A6: ((k + 1) + 1) |-> (0. K) = ((k + 1) |-> (0. K)) ^ <*(0. K)*> by FINSEQ_2:60;

assume S

then the multF of K $$ (((k + 1) + 1) |-> (0. K)) = (0. K) * (0. K) by A6, FINSOP_1:4

.= 0. K ;

hence S

(n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)

proof

len (n |-> (0. K)) = n
by CARD_1:def 7;
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: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: verum

end;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: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: verum

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

for k being Nat holds S

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

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

proof

A18:
for B9 being Element of Fin (Permutations n) st B9 c= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
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 A16, FUNCOP_1:7; :: thesis: verum

end;G0 . {.x.} = 0. K by FUNCOP_1:7;

hence G0 . {x} = (PPath_product (0. (K,n,n))) . x by A16, FUNCOP_1:7; :: thesis: verum

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))

proof

Permutations n in Fin (Permutations n)
by FINSUB_1:def 5;
let B9 be Element of Fin (Permutations n); :: thesis: ( B9 c= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} implies 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)) )

assume that

B9 c= In ((Permutations n),(Fin (Permutations n))) and

B9 <> {} ; :: thesis: 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))

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

end;G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) )

assume that

B9 c= In ((Permutations n),(Fin (Permutations n))) and

B9 <> {} ; :: thesis: 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))

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

proof

let x be Element of Permutations n; :: thesis: ( x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) )

assume x in (In ((Permutations n),(Fin (Permutations n)))) \ 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 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: verum

end;assume x in (In ((Permutations n),(Fin (Permutations n)))) \ 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 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: verum

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