defpred S₁[ Nat, Nat, set ] means $3 = pow (x,(($1 - 1) * ($2 - 1)));
reconsider m9 = m as Element of NAT by ORDINAL1:def 12;
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] ;
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(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:1, MATRIX_1:24;
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:1;
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