let D be non empty set ; for M being Matrix of D
for k, l being Nat st k in dom (Mx2FinS M) & l = k - 1 holds
( [((l div (width M)) + 1),((l mod (width M)) + 1)] in Indices M & (Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1)) )
let M be Matrix of D; for k, l being Nat st k in dom (Mx2FinS M) & l = k - 1 holds
( [((l div (width M)) + 1),((l mod (width M)) + 1)] in Indices M & (Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1)) )
let k, l be Nat; ( k in dom (Mx2FinS M) & l = k - 1 implies ( [((l div (width M)) + 1),((l mod (width M)) + 1)] in Indices M & (Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1)) ) )
assume that
A1:
k in dom (Mx2FinS M)
and
A2:
l = k - 1
; ( [((l div (width M)) + 1),((l mod (width M)) + 1)] in Indices M & (Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1)) )
set jj = (l mod (width M)) + 1;
set ii = (l div (width M)) + 1;
A3:
len (Mx2FinS M) = (len M) * (width M)
by Th39;
k in Seg (len (Mx2FinS M))
by A1, FINSEQ_1:def 3;
then
k <= len (Mx2FinS M)
by FINSEQ_1:1;
then
k < ((len M) * (width M)) + 1
by A3, NAT_1:13;
then A4:
k - 1 < (((len M) * (width M)) + 1) - 1
by XREAL_1:9;
A5:
Mx2FinS M <> {}
by A1;
then A6:
width M <> 0
by A3;
A7:
width M > 0
by A5, A3;
then A8:
l = ((l div (width M)) * (width M)) + (l mod (width M))
by NAT_D:2;
width M divides (len M) * (width M)
by NAT_D:def 3;
then
l div (width M) < ((len M) * (width M)) div (width M)
by A2, A6, A4, Th1;
then
l div (width M) < len M
by A6, NAT_D:18;
then A9:
(l div (width M)) + 1 <= len M
by NAT_1:13;
l mod (width M) < width M
by A7, NAT_D:1;
then A10:
(l mod (width M)) + 1 <= width M
by NAT_1:13;
(l mod (width M)) + 1 >= 1
by NAT_1:11;
then A11:
(l mod (width M)) + 1 in Seg (width M)
by A10, FINSEQ_1:1;
(l div (width M)) + 1 >= 1
by NAT_1:11;
then
(l div (width M)) + 1 in Seg (len M)
by A9, FINSEQ_1:1;
hence
[((l div (width M)) + 1),((l mod (width M)) + 1)] in Indices M
by A11, MATRPROB:12; (Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1))
then M * (((l div (width M)) + 1),((l mod (width M)) + 1)) =
(Mx2FinS M) . (((((l div (width M)) + 1) - 1) * (width M)) + ((l mod (width M)) + 1))
by Th40
.=
(Mx2FinS M) . k
by A2, A8
;
hence
(Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1))
; verum