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