let M1, M2 be Matrix of m,L; :: thesis: ( ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M1 * (i,j) = pow (x,((i - 1) * (j - 1))) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) implies M1 = M2 )
assume A4: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M1 * (i,j) = pow (x,((i - 1) * (j - 1))) ; :: thesis: ( ex i, j being Nat st
( 1 <= i & i <= m & 1 <= j & j <= m & not M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) or M1 = M2 )
assume A5: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ; :: thesis: M1 = M2

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) )
A6: Indices M1 = [:(Seg m),(Seg m):] by MATRIX_0:24;
assume [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
then ex x, y being object st
( x in Seg m & y in Seg m & [x,y] = [i,j] ) by A6, ZFMISC_1:def 2;
then consider z, y being set such that
A7: [i,j] = [z,y] and
A8: z in Seg m and
A9: y in Seg m ;
j = y by A7, XTUPLE_0:1;
then A10: ( 1 <= j & j <= m ) by A9, FINSEQ_1:1;
i = z by A7, XTUPLE_0:1;
then A11: ( 1 <= i & i <= m ) by A8, FINSEQ_1:1;
hence M1 * (i,j) = pow (x,((i - 1) * (j - 1))) by A4, A10
.= M2 * (i,j) by A5, A11, A10 ;
:: thesis: verum

end;

hence M1 = M2 by MATRIX_0:27; :: thesis: verum