defpred S₁[ Nat, Nat, set ] means $3 = pow x,(($1 - 1) * ($2 - 1));
reconsider m9 = m as Element of NAT by ORDINAL1:def 13;
A1: for i, j being Nat st [i,j] in [:(Seg m9),(Seg m9):] holds
ex x being Element of L st S₁[i,j,x] ;
A2: for i, j being Nat st [i,j] in [:(Seg m9),(Seg m9):] holds
for x1, x2 being Element of L st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
consider M being Matrix of m9,m9,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(A2, A1);
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 ( 1 <= i & i <= m ) ; :: thesis: for j being Nat st 1 <= j & j <= m holds
M * i,j = pow x,((i - 1) * (j - 1))
then A4: ( Indices M = [:(Seg m),(Seg m):] & i in Seg m ) by FINSEQ_1:3, MATRIX_1:25;
let j be Nat; :: thesis: ( 1 <= j & j <= m implies M * i,j = pow x,((i - 1) * (j - 1)) )
assume ( 1 <= j & j <= m ) ; :: thesis: M * i,j = pow x,((i - 1) * (j - 1))
then j in Seg m by FINSEQ_1:3;
then [i,j] in Indices M by A4, 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