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 ((),(Fin ()))),()) = 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 ((),(Fin ()))),()) = 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 ((),(Fin ()))),()) = 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 ((),(Fin ()));
Permutations n1 in Fin () by FINSUB_1:def 5;
then reconsider P1 = In ((),(Fin ())) as non empty Element of Fin () by SUBSET_1:def 8;
defpred S1[ non empty Element of Fin ()] means the addF of K \$\$ (\$1,()) = 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 ((),(Fin ()))),()) = 0. K
A2: for x being Element of Permutations n1
for B being non empty Element of Fin () st x in P1 & B c= P1 & not x in B & S1[B] holds
S1[B \/ {.x.}]
proof
let x be Element of Permutations n1; :: thesis: for B being non empty Element of Fin () st x in P1 & B c= P1 & not x in B & S1[B] holds
S1[B \/ {.x.}]

let B be non empty Element of Fin (); :: thesis: ( x in P1 & B c= P1 & not x in B & S1[B] implies S1[B \/ {.x.}] )
assume that
x in P1 and
B c= P1 and
A3: not x in B and
A4: S1[B] ; :: thesis: S1[B \/ {.x.}]
the addF of K \$\$ ((B \/ {.x.}),()) = the addF of K . (( the addF of K \$\$ (B,())),(() . x)) by
.= ( the addF of K \$\$ (B,())) + (0. K) by
.= 0. K by ;
hence S1[B \/ {.x.}] ; :: thesis: verum
end;
A5: for x being Element of Permutations n1 st x in P1 holds
S1[{.x.}]
proof
let x be Element of Permutations n1; :: thesis: ( x in P1 implies S1[{.x.}] )
assume x in P1 ; :: thesis: S1[{.x.}]
the addF of K \$\$ ({.x.},()) = () . x by SETWISEO:17
.= 0. K by ;
hence S1[{.x.}] ; :: thesis: verum
end;
S1[P1] from MATRIX_9:sch 1(A5, A2);
hence the addF of K \$\$ ((In ((),(Fin ()))),()) = 0. K ; :: thesis: verum