let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( [((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; :: thesis: (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)) ; :: thesis: verum