let M1, M2 be Matrix of m,1,L; :: thesis: ( ( for i being Nat st 1 <= i & i <= m holds
M1 * (i,1) = p . (i - 1) ) & ( for i being Nat st 1 <= i & i <= m holds
M2 * (i,1) = p . (i - 1) ) implies M1 = M2 )
assume that
A5: for i being Nat st 1 <= i & i <= m holds
M1 * (i,1) = p . (i - 1) and
A6: for i being Nat st 1 <= i & i <= m holds
M2 * (i,1) = p . (i - 1) ; :: thesis: M1 = M2

per cases ( m = 0 or m > 0 ) ;

suppose A7: m = 0 ; :: thesis: M1 = M2

then A8: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) by MATRIX_0:22;
A9: width M1 = 0 by A7, MATRIX_0:22
.= width M2 by A7, MATRIX_0:22 ;
len M1 = 0 by A7, MATRIX_0:22
.= len M2 by A7, MATRIX_0:22 ;
hence M1 = M2 by A9, A8, MATRIX_0:21; :: thesis: verum

end;

suppose A10: m > 0 ; :: thesis: M1 = M2

A11: now :: thesis: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
then A12: [i,j] in [:(Seg m),(Seg 1):] by A10, MATRIX_0:23;
then [i,j] `2 in Seg 1 by MCART_1:10;
then j in Seg 1 ;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A13: j = 1 by XXREAL_0:1;
[i,j] `1 in Seg m by A12, MCART_1:10;
then i in Seg m ;
then A14: ( 1 <= i & i <= m ) by FINSEQ_1:1;
hence M1 * (i,j) = p . (i - 1) by A5, A13
.= M2 * (i,j) by A6, A14, A13 ;
:: thesis: verum

end;

A15: width M1 = 1 by A10, MATRIX_0:23
.= width M2 by A10, MATRIX_0:23 ;
len M1 = m by A10, MATRIX_0:23
.= len M2 by A10, MATRIX_0:23 ;
hence M1 = M2 by A15, A11, MATRIX_0:21; :: thesis: verum

end;

end;