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_{1}[ 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_{1}[B] holds

S_{1}[B \/ {.x.}]

S_{1}[{.x.}]
_{1}[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

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

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

S

proof

A5:
for x being Element of Permutations n1 st x in P1 holds
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_{1}[B] holds

S_{1}[B \/ {.x.}]

let B be non empty Element of Fin (Permutations n1); :: thesis: ( x in P1 & B c= P1 & not x in B & S_{1}[B] implies S_{1}[B \/ {.x.}] )

assume that

x in P1 and

B c= P1 and

A3: not x in B and

A4: S_{1}[B]
; :: thesis: S_{1}[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_{1}[B \/ {.x.}]
; :: thesis: verum

end;S

let B be non empty Element of Fin (Permutations n1); :: thesis: ( x in P1 & B c= P1 & not x in B & S

assume that

x in P1 and

B c= P1 and

A3: not x in B and

A4: S

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

S

proof

S
let x be Element of Permutations n1; :: thesis: ( x in P1 implies S_{1}[{.x.}] )

assume x in P1 ; :: thesis: S_{1}[{.x.}]

the addF of K $$ ({.x.},(PPath_product M1)) = (PPath_product M1) . x by SETWISEO:17

.= 0. K by A1, Th52 ;

hence S_{1}[{.x.}]
; :: thesis: verum

end;assume x in P1 ; :: thesis: S

the addF of K $$ ({.x.},(PPath_product M1)) = (PPath_product M1) . x by SETWISEO:17

.= 0. K by A1, Th52 ;

hence S

hence the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) = 0. K ; :: thesis: verum