let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) = 0. K
let K be Field; :: thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) = 0. K
let M be Matrix of n,K; :: thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) = 0. K )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider M1 = M as Matrix of n1,K ;
set F = the addF of K;
set f = PPath_product M1;
set P1 = In ((Permutations n1),(Fin (Permutations n1)));
Permutations n1 in Fin (Permutations n1) by FINSUB_1:def 5;
then reconsider P1 = In ((Permutations n1),(Fin (Permutations n1))) as non empty Element of Fin (Permutations n1) by SUBSET_1:def 8;
defpred S₁[ non empty Element of Fin (Permutations n1)] means the addF of K $$ ($1,(PPath_product M1)) = 0. K;
assume A1: ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; :: thesis: the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) = 0. K
A2: for x being Element of Permutations n1
for B being non empty Element of Fin (Permutations n1) st x in P1 & B c= P1 & not x in B & S₁[B] holds
S₁[B \/ {.x.}]

proof

let x be Element of Permutations n1; :: thesis: for B being non empty Element of Fin (Permutations n1) st x in P1 & B c= P1 & not x in B & S₁[B] holds
S₁[B \/ {.x.}]
let B be non empty Element of Fin (Permutations n1); :: thesis: ( x in P1 & B c= P1 & not x in B & S₁[B] implies S₁[B \/ {.x.}] )
assume that
x in P1 and
B c= P1 and
A3: not x in B and
A4: S₁[B] ; :: thesis: S₁[B \/ {.x.}]
the addF of K $$ ((B \/ {.x.}),(PPath_product M1)) = the addF of K . (( the addF of K $$ (B,(PPath_product M1))),((PPath_product M1) . x)) by A3, SETWOP_2:2
.= ( the addF of K $$ (B,(PPath_product M1))) + (0. K) by A1, Th52
.= 0. K by A4, RLVECT_1:4 ;
hence S₁[B \/ {.x.}] ; :: thesis: verum

end;

A5: for x being Element of Permutations n1 st x in P1 holds
S₁[{.x.}]

proof

let x be Element of Permutations n1; :: thesis: ( x in P1 implies S₁[{.x.}] )
assume x in P1 ; :: thesis: S₁[{.x.}]
the addF of K $$ ({.x.},(PPath_product M1)) = (PPath_product M1) . x by SETWISEO:17
.= 0. K by A1, Th52 ;
hence S₁[{.x.}] ; :: thesis: verum

end;

S₁[P1] from MATRIX_9:sch 1(A5, A2);
hence the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) = 0. K ; :: thesis: verum