defpred S1[ 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 S1[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
S1[i,j,M * (i,j)]
from MATRIX_0:sch 2(A1);
reconsider M = M as Matrix of m,m,L ;
take
M
; 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 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)))let i be
Nat;
( 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 )
;
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;
( 1 <= j & j <= m implies M * (i,j) = pow (x,((i - 1) * (j - 1))) )assume
( 1
<= j &
j <= m )
;
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;
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)))
; verum