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
A9: for i being Nat st 1 <= i & i <= m holds
M1 * i,1 = p . (i - 1) and
A10: 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 A11: m = 0 ; :: thesis: M1 = M2

then A12: len M1 = 0 by MATRIX_1:23
.= len M2 by A11, MATRIX_1:23 ;
A13: width M1 = 0 by A11, MATRIX_1:23
.= width M2 by A11, MATRIX_1:23 ;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j = M2 * i,j by A11, MATRIX_1:23;
hence M1 = M2 by A12, A13, MATRIX_1:21; :: thesis: verum

end;

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

then A15: len M1 = m by MATRIX_1:24
.= len M2 by A14, MATRIX_1:24 ;
A16: width M1 = 1 by A14, MATRIX_1:24
.= width M2 by A14, MATRIX_1:24 ;

now

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 A17: [i,j] in [:(Seg m),(Seg 1):] by A14, MATRIX_1:24;
then [i,j] `1 in Seg m by MCART_1:10;
then i in Seg m by MCART_1:def 1;
then A18: ( 1 <= i & i <= m ) by FINSEQ_1:3;
[i,j] `2 in Seg 1 by A17, MCART_1:10;
then j in Seg 1 by MCART_1:def 2;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:3;
then A19: j = 1 by XXREAL_0:1;
hence M1 * i,j = p . (i - 1) by A9, A18
.= M2 * i,j by A10, A18, A19 ;
:: thesis: verum

end;

hence M1 = M2 by A15, A16, MATRIX_1:21; :: thesis: verum

end;

end;