let n be Element of NAT ; :: thesis: for K being Field
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p
let K be Field; :: thesis: for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p
let p be Element of Permutations n; :: thesis: for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p
let A be Matrix of n,K; :: thesis: ( n >= 1 implies (Path_product (A @)) . (p ") = (Path_product A) . p )
assume A1: n >= 1 ; :: thesis: (Path_product (A @)) . (p ") = (Path_product A) . p
A2: len (Path_matrix (p,A)) = n by MATRIX_3:def 7;
then reconsider g = (Path_matrix (p,A)) * (p ") as FinSequence of K by A1, Th34;
(Path_product (A @)) . (p ") = - (( the multF of K $$ (Path_matrix ((p "),(A @)))),(p ")) by MATRIX_3:def 8
.= - (( the multF of K $$ g),(p ")) by A1, Th35
.= - (( the multF of K $$ g),p) by A1, Th29
.= - (( the multF of K $$ (Path_matrix (p,A))),p) by A2, Th31, Th32 ;
hence (Path_product (A @)) . (p ") = (Path_product A) . p by MATRIX_3:def 8; :: thesis: verum