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

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 )
;

end;

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;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

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

.= 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;

A11: now :: thesis: for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = M2 * (i,j)

A15: width M1 =
1
by A10, MATRIX_0:23
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;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

.= 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