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 A7: 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 A8: 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 )
assume A9: [i,j] in Indices M1 ; :: thesis: M1 * i,j = M2 * i,j
Indices M1 = [:(Seg m),(Seg m):] by MATRIX_1:25;
then ex x, y being set st
( x in Seg m & y in Seg m & [x,y] = [i,j] ) by A9, ZFMISC_1:def 2;
then consider z, y being set such that
A10: ( [i,j] = [z,y] & z in Seg m & y in Seg m ) ;
A11: i = [z,y] `1 by A10, MCART_1:def 1
.= z by MCART_1:def 1 ;
j = [z,y] `2 by A10, MCART_1:def 2
.= y by MCART_1:def 2 ;
then A12: ( 1 <= i & i <= m & 1 <= j & j <= m ) by A10, A11, FINSEQ_1:3;
hence M1 * i,j = pow x,((i - 1) * (j - 1)) by A7
.= M2 * i,j by A8, A12 ;
:: thesis: verum

end;

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