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)))),(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 $$ ((In ((Permutations n),(Fin (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 $$ ((In ((Permutations n),(Fin (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 $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) = 0. K

set P1 = In ((Permutations n),(Fin (Permutations n)));

set f = Path_product M1;

set F = the addF of K;

Permutations n in Fin (Permutations n) by FINSUB_1:def 5;

then In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;

then reconsider P1 = In ((Permutations n),(Fin (Permutations n))) as non empty Element of Fin (Permutations n1) ;

defpred S_{1}[ 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_{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)))),(Path_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)))),(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 $$ ((In ((Permutations n),(Fin (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 $$ ((In ((Permutations n),(Fin (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 $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) = 0. K

set P1 = In ((Permutations n),(Fin (Permutations n)));

set f = Path_product M1;

set F = the addF of K;

Permutations n in Fin (Permutations n) by FINSUB_1:def 5;

then In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;

then reconsider P1 = In ((Permutations n),(Fin (Permutations n))) as non empty Element of Fin (Permutations n1) ;

defpred S

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.}),(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_{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.}),(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

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.},(Path_product M1)) = (Path_product M1) . x by SETWISEO:17

.= 0. K by A1, Th50 ;

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

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

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

.= 0. K by A1, Th50 ;

hence S

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