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

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

end;

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

A12: 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 A13: [i,j] in [:(Seg m),(Seg 1):] by A11, MATRIX_1:23;
then [i,j] `2 in Seg 1 by MCART_1:10;
then j in Seg 1 by MCART_1:def 2;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A14: j = 1 by XXREAL_0:1;
[i,j] `1 in Seg m by A13, MCART_1:10;
then i in Seg m by MCART_1:def 1;
then A15: ( 1 <= i & i <= m ) by FINSEQ_1:1;
hence M1 * (i,j) = p . (i - 1) by A6, A14
.= M2 * (i,j) by A7, A15, A14 ;
:: thesis: verum

end;

A16: width M1 = 1 by A11, MATRIX_1:23
.= width M2 by A11, MATRIX_1:23 ;
len M1 = m by A11, MATRIX_1:23
.= len M2 by A11, MATRIX_1:23 ;
hence M1 = M2 by A16, A12, MATRIX_1:21; :: thesis: verum

end;

end;