let n be Nat; :: thesis: for K being commutative Ring
for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
let K be commutative Ring; :: thesis: for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n & i < j implies for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p) )
assume that
A1: i in Seg n and
A2: j in Seg n and
A3: i < j ; :: thesis: for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
{i,j} in 2Set (Seg n) by A1, A2, A3, Th1;
then reconsider n2 = n - 2 as Nat by Th2, NAT_1:21, NAT_1:23;
let M be Matrix of n,K; :: thesis: ( Line (M,i) = Line (M,j) implies for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p) )
assume A4: Line (M,i) = Line (M,j) ; :: thesis: for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
reconsider M9 = M as Matrix of n2 + 2,K ;
let p, q, tr be Element of Permutations n; :: thesis: ( q = p * tr & tr is being_transposition & tr . i = j implies (Path_product M) . q = - ((Path_product M) . p) )
assume that
A5: q = p * tr and
A6: tr is being_transposition and
A7: tr . i = j ; :: thesis: (Path_product M) . q = - ((Path_product M) . p)
reconsider TR = tr as Permutation of (Seg (n2 + 2)) by MATRIX_1:def 12;
set Mt = M9 * TR;
A8: for k being Nat st 1 <= k & k <= len M9 holds
M9 . k = (M9 * TR) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len M9 implies M9 . k = (M9 * TR) . k )
assume that
A9: 1 <= k and
A10: k <= len M9 ; :: thesis: M9 . k = (M9 * TR) . k
A11: k in Seg (len M9) by A9, A10;
A12: Line (M,j) = M . j by A2, MATRIX_0:52;
A13: dom TR = Seg n by FUNCT_2:52;
A14: Line (M,i) = M . i by A1, MATRIX_0:52;
A15: len M9 = n by MATRIX_0:def 2;
then A16: Line ((M9 * TR),k) = M . (tr . k) by A11, Th38;

per cases ( k = i or k = j or ( k <> i & k <> j ) ) ;

suppose k = i ; :: thesis: M9 . k = (M9 * TR) . k

hence M9 . k = (M9 * TR) . k by A1, A4, A7, A16, A14, A12, MATRIX_0:52; :: thesis: verum

end;

suppose A17: k = j ; :: thesis: M9 . k = (M9 * TR) . k

then A18: M . k = M . i by A2, A4, A14, MATRIX_0:52;
Line ((M9 * TR),k) = M . i by A3, A6, A7, A16, A17, Th8;
hence M9 . k = (M9 * TR) . k by A2, A17, A18, MATRIX_0:52; :: thesis: verum

end;

suppose ( k <> i & k <> j ) ; :: thesis: M9 . k = (M9 * TR) . k

then Line ((M9 * TR),k) = M . k by A3, A6, A7, A11, A15, A13, A16, Th8;
hence M9 . k = (M9 * TR) . k by A11, A15, MATRIX_0:52; :: thesis: verum

end;

end;

end;

len (M9 * TR) = len M9 by Def4;
then A19: M9 * TR = M by A8;
reconsider Tr = tr, p2 = p as Element of Permutations (n2 + 2) ;
A20: sgn (Tr,K) = - (1_ K) by A6, Th14;
tr = tr " by A6, Th20;
hence (Path_product M) . q = (- (1_ K)) * ((Path_product M9) . p2) by A5, A19, A20, Th43
.= - ((1_ K) * ((Path_product M9) . p2)) by VECTSP_1:9
.= - ((Path_product M) . p) ;
:: thesis: verum