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

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)

hence
M1 = M2
by MATRIX_0:27; :: thesis: verumM1 * (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;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