reconsider m' = m as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Nat, Nat, set ] means $3 = pow x,(($1 - 1) * ($2 - 1));
A1: for i, j being Nat st [i,j] in [:(Seg m'),(Seg m'):] holds
for x1, x2 being Element of L st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
A2: for i, j being Nat st [i,j] in [:(Seg m'),(Seg m'):] holds
ex x being Element of L st S₁[i,j,x] ;
consider M being Matrix of m',m',L such that
A3: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * i,j] from MATRIX_1:sch 2(A1, A2);
reconsider M = M as Matrix of m,m,L ;
take M ; :: thesis: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M * i,j = pow x,((i - 1) * (j - 1))

now

let i be Nat; :: thesis: ( 1 <= i & i <= m implies for j being Nat st 1 <= j & j <= m holds
M * i,j = pow x,((i - 1) * (j - 1)) )
assume A4: ( 1 <= i & i <= m ) ; :: thesis: for j being Nat st 1 <= j & j <= m holds
M * i,j = pow x,((i - 1) * (j - 1))
let j be Nat; :: thesis: ( 1 <= j & j <= m implies M * i,j = pow x,((i - 1) * (j - 1)) )
assume A5: ( 1 <= j & j <= m ) ; :: thesis: M * i,j = pow x,((i - 1) * (j - 1))
A6: Indices M = [:(Seg m),(Seg m):] by MATRIX_1:25;
( i in Seg m & j in Seg m ) by A4, A5, FINSEQ_1:3;
then [i,j] in Indices M by A6, ZFMISC_1:def 2;
hence M * i,j = pow x,((i - 1) * (j - 1)) by A3; :: thesis: verum

end;

hence for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
M * i,j = pow x,((i - 1) * (j - 1)) ; :: thesis: verum