let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for perm being Element of Permutations n st perm <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) holds
(Path_product M) . perm = 0. K
let K be Field; :: thesis: for M being Matrix of n,K
for perm being Element of Permutations n st perm <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) holds
(Path_product M) . perm = 0. K
let M be Matrix of n,K; :: thesis: for perm being Element of Permutations n st perm <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) holds
(Path_product M) . perm = 0. K
let p be Element of Permutations n; :: thesis: ( p <> idseq n & ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) implies (Path_product M) . p = 0. K )
assume that
A1: p <> idseq n and
A2: ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) ; :: thesis: (Path_product M) . p = 0. K
reconsider p9 = p as Permutation of (Seg n) by MATRIX_1:def 12;
set PP = Path_product M;
set PATH = Path_matrix (p,M);

now :: thesis: ex i being Nat st
( i in dom (Path_matrix (p,M)) & (Path_matrix (p,M)) . i = 0. K )

per cases ( M is lower_triangular Matrix of n,K or M is upper_triangular Matrix of n,K ) by A2;

suppose A3: M is lower_triangular Matrix of n,K ; :: thesis: ex i being Nat st
( i in dom (Path_matrix (p,M)) & (Path_matrix (p,M)) . i = 0. K )

A4: rng p9 = Seg n by FUNCT_2:def 3;
A5: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
consider i being Nat such that
A6: i in Seg n and
A7: p . i > i by A1, Th4;
reconsider Pi = p . i as Nat ;
dom p9 = Seg n by FUNCT_2:52;
then p9 . i in Seg n by A6, A4, FUNCT_1:def 3;
then [i,Pi] in [:(Seg n),(Seg n):] by A6, ZFMISC_1:87;
then A8: M * (i,Pi) = 0. K by A3, A7, A5, MATRIX_1:def 9;
len (Path_matrix (p,M)) = n by MATRIX_3:def 7;
then A9: dom (Path_matrix (p,M)) = Seg n by FINSEQ_1:def 3;
then (Path_matrix (p,M)) . i = M * (i,Pi) by A6, MATRIX_3:def 7;
hence ex i being Nat st
( i in dom (Path_matrix (p,M)) & (Path_matrix (p,M)) . i = 0. K ) by A6, A9, A8; :: thesis: verum

end;

suppose A10: M is upper_triangular Matrix of n,K ; :: thesis: ex i being Nat st
( i in dom (Path_matrix (p,M)) & (Path_matrix (p,M)) . i = 0. K )

A11: rng p9 = Seg n by FUNCT_2:def 3;
A12: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
consider i being Nat such that
A13: i in Seg n and
A14: p . i < i by A1, Th4;
reconsider Pi = p . i as Nat ;
dom p9 = Seg n by FUNCT_2:52;
then p9 . i in Seg n by A13, A11, FUNCT_1:def 3;
then [i,Pi] in [:(Seg n),(Seg n):] by A13, ZFMISC_1:87;
then A15: M * (i,Pi) = 0. K by A10, A14, A12, MATRIX_1:def 8;
len (Path_matrix (p,M)) = n by MATRIX_3:def 7;
then A16: dom (Path_matrix (p,M)) = Seg n by FINSEQ_1:def 3;
then (Path_matrix (p,M)) . i = M * (i,Pi) by A13, MATRIX_3:def 7;
hence ex i being Nat st
( i in dom (Path_matrix (p,M)) & (Path_matrix (p,M)) . i = 0. K ) by A13, A16, A15; :: thesis: verum

end;

end;

end;

then Product (Path_matrix (p,M)) = 0. K by FVSUM_1:82;
then A17: (Path_product M) . p = - ((0. K),p) by MATRIX_3:def 8;
( - ((0. K),p) = 0. K or - ((0. K),p) = - (0. K) ) by MATRIX_1:def 16;
hence (Path_product M) . p = 0. K by A17, RLVECT_1:12; :: thesis: verum