let D be non empty set ; :: thesis: for Rseq being Function of [:NAT,NAT:],D
for n, m being Nat ex M being Matrix of n + 1,m + 1,D st
for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1))
let Rseq be Function of [:NAT,NAT:],D; :: thesis: for n, m being Nat ex M being Matrix of n + 1,m + 1,D st
for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1))
let n, m be Nat; :: thesis: ex M being Matrix of n + 1,m + 1,D st
for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1))
defpred S₁[ Nat, Nat, object ] means ex i1, j1 being Nat st
( i1 = $1 - 1 & j1 = $2 - 1 & $3 = Rseq . (i1,j1) );

A1: now :: thesis: for i, j being Nat st [i,j] in [:(Seg (n + 1)),(Seg (m + 1)):] holds
ex x being Element of D st S₁[i,j,x]

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg (n + 1)),(Seg (m + 1)):] implies ex x being Element of D st S₁[i,j,x] )
assume [i,j] in [:(Seg (n + 1)),(Seg (m + 1)):] ; :: thesis: ex x being Element of D st S₁[i,j,x]
then ( [i,j] `1 in Seg (n + 1) & [i,j] `2 in Seg (m + 1) ) by MCART_1:10;
then ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then reconsider i1 = i - 1, j1 = j - 1 as Element of NAT by NAT_1:21;
reconsider i1 = i1, j1 = j1 as Nat ;
dom Rseq = [:NAT,NAT:] by FUNCT_2:def 1;
then [i1,j1] in dom Rseq by ZFMISC_1:def 2;
then reconsider x = Rseq . (i1,j1) as Element of D by FUNCT_2:5;
take x = x; :: thesis: S₁[i,j,x]
thus S₁[i,j,x] ; :: thesis: verum

end;

consider M being Matrix of n + 1,m + 1,D such that
A2: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * (i,j)] from MATRIX_0:sch 2(A1);
take M ; :: thesis: for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1))

hereby :: thesis: verum

let i, j be Nat; :: thesis: ( i <= n & j <= m implies Rseq . (i,j) = M * ((i + 1),(j + 1)) )
assume ( i <= n & j <= m ) ; :: thesis: Rseq . (i,j) = M * ((i + 1),(j + 1))
then ( i < n + 1 & j < m + 1 ) by NAT_1:13;
then ( i + 1 in Seg (n + 1) & j + 1 in Seg (m + 1) ) by FINSEQ_3:11;
then [(i + 1),(j + 1)] in [:(Seg (n + 1)),(Seg (m + 1)):] by ZFMISC_1:def 2;
then [(i + 1),(j + 1)] in Indices M by MATRIX_0:23;
then consider i1, j1 being Nat such that
A4: ( i1 = (i + 1) - 1 & j1 = (j + 1) - 1 & M * ((i + 1),(j + 1)) = Rseq . (i1,j1) ) by A2;
thus Rseq . (i,j) = M * ((i + 1),(j + 1)) by A4; :: thesis: verum

end;