let n be Nat; :: thesis: for K being commutative Ring
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 commutative Ring; :: 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, Th33;
(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, Th34
.= - (( the multF of K $$ g),p) by A1, Th28
.= - (( the multF of K $$ (Path_matrix (p,A))),p) by A2, Th30, Th31 ;
hence (Path_product (A @)) . (p ") = (Path_product A) . p by MATRIX_3:def 8; :: thesis: verum