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 $$ (FinOmega (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 $$ (FinOmega (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 $$ (FinOmega (Permutations n)),(PPath_product M) = 0. K )
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
reconsider M1 = M as Matrix of n1,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 $$ (FinOmega (Permutations n)),(PPath_product M) = 0. K
set F = the addF of K;
set f = PPath_product M1;
set P1 = FinOmega (Permutations n1);
consider c being Element of Permutations n;
reconsider P1 = FinOmega (Permutations n1) as non empty Element of Fin (Permutations n1) by MATRIX_2:30, MATRIX_2:def 17;
defpred S₁[ non empty Element of Fin (Permutations n1)] means the addF of K $$ $1,(PPath_product M1) = 0. K;
A2: 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:26
.= 0. K by A1, Th52 ;
hence S₁[{.x.}] ; :: thesis: verum

end;

A3: 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 A4: ( x in P1 & B c= P1 & not x in B & S₁[B] ) ; :: thesis: S₁[B \/ {.x.}]
then 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 SETWOP_2:4
.= (the addF of K $$ B,(PPath_product M1)) + (0. K) by A1, Th52
.= 0. K by A4, RLVECT_1:10 ;
hence S₁[B \/ {.x.}] ; :: thesis: verum

end;

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