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)),(Path_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)),(Path_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)),(Path_product M)) = 0. K )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider M1 = M as Matrix of n1,K ;
given i being Element of NAT such that A1: ( 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)),(Path_product M)) = 0. K
set P1 = FinOmega (Permutations n);
set f = Path_product M1;
set F = the addF of K;
reconsider P1 = FinOmega (Permutations n) as non empty Element of Fin (Permutations n1) by MATRIX_2:26, MATRIX_2:def 14;
defpred S₁[ non empty Element of Fin (Permutations n1)] means the addF of K $$ ($1,(Path_product M1)) = 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.}),(Path_product M1)) = the addF of K . (( the addF of K $$ (B,(Path_product M1))),((Path_product M1) . x)) by A3, SETWOP_2:2
.= ( the addF of K $$ (B,(Path_product M1))) + (0. K) by A1, Th50
.= 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.},(Path_product M1)) = (Path_product M1) . x by SETWISEO:17
.= 0. K by A1, Th50 ;
hence S₁[{.x.}] ; :: thesis: verum

end;

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