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 A5: 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 A6: 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

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
A7: Indices M1 = [:(Seg m),(Seg m):] by MATRIX_1:24;
assume [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
then ex x, y being set st
( x in Seg m & y in Seg m & [x,y] = [i,j] ) by A7, ZFMISC_1:def 2;
then consider z, y being set such that
A8: [i,j] = [z,y] and
A9: z in Seg m and
A10: y in Seg m ;
j = [z,y] `2 by A8, MCART_1:def 2
.= y by MCART_1:def 2 ;
then A11: ( 1 <= j & j <= m ) by A10, FINSEQ_1:1;
i = [z,y] `1 by A8, MCART_1:def 1
.= z by MCART_1:def 1 ;
then A12: ( 1 <= i & i <= m ) by A9, FINSEQ_1:1;
hence M1 * (i,j) = pow (x,((i - 1) * (j - 1))) by A5, A11
.= M2 * (i,j) by A6, A12, A11 ;
:: thesis: verum

end;

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