defpred S_{1}[ 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_{1}[i,j,x]
;

consider M being Matrix of m9,m9,L such that

A2: for i, j being Nat st [i,j] in Indices M holds

S_{1}[i,j,M * (i,j)]
from MATRIX_0: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)))

M * (i,j) = pow (x,((i - 1) * (j - 1))) ; :: thesis: verum

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

consider M being Matrix of m9,m9,L such that

A2: for i, j being Nat st [i,j] in Indices M holds

S

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 :: thesis: for i being Nat st 1 <= i & i <= m holds

for j being Nat st 1 <= j & j <= m holds

M * (i,j) = pow (x,((i - 1) * (j - 1)))

hence
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds for j being Nat st 1 <= j & j <= m holds

M * (i,j) = pow (x,((i - 1) * (j - 1)))

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 A3: ( Indices M = [:(Seg m),(Seg m):] & i in Seg m ) by MATRIX_0: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 ;

then [i,j] in Indices M by A3, ZFMISC_1:def 2;

hence M * (i,j) = pow (x,((i - 1) * (j - 1))) by A2; :: thesis: verum

end;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 A3: ( Indices M = [:(Seg m),(Seg m):] & i in Seg m ) by MATRIX_0: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 ;

then [i,j] in Indices M by A3, ZFMISC_1:def 2;

hence M * (i,j) = pow (x,((i - 1) * (j - 1))) by A2; :: thesis: verum

M * (i,j) = pow (x,((i - 1) * (j - 1))) ; :: thesis: verum