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_2:def 11;
set PP = Path_product M;
set PATH = Path_matrix p,M;

now

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_1:25;
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:67;
then p9 . i in Seg n by A6, A4, FUNCT_1:def 5;
then [i,Pi] in [:(Seg n),(Seg n):] by A6, ZFMISC_1:106;
then A8: M * i,Pi = 0. K by A3, A7, A5, MATRIX_2:def 4;
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_1:25;
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:67;
then p9 . i in Seg n by A13, A11, FUNCT_1:def 5;
then [i,Pi] in [:(Seg n),(Seg n):] by A13, ZFMISC_1:106;
then A15: M * i,Pi = 0. K by A10, A14, A12, MATRIX_2:def 3;
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:107;
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_2:def 16;
hence (Path_product M) . p = 0. K by A17, RLVECT_1:25; :: thesis: verum
set mm = the multF of K;