let D be non empty set ; :: thesis:
let M be Matrix of D; :: thesis:
let k, l be Element of NAT ; :: thesis:
assume A1: ( k in dom (Mx2FinS M) & l = k - 1 ) ; :: thesis:
A2: Mx2FinS M <> {} by A1, RELAT_1:60;
A3: len (Mx2FinS M) = (len M) * (width M) by Th39;
then A4: ( len M <> 0 & width M <> 0 ) by A2;
A5: ( len M > 0 & width M > 0 ) by A2, A3;
set ii = (l div (width M)) + 1;
set jj = (l mod (width M)) + 1;
k in Seg (len (Mx2FinS M)) by A1, FINSEQ_1:def 3;
then ( k >= 1 & k <= len (Mx2FinS M) ) by FINSEQ_1:3;
then k < ((len M) * (width M)) + 1 by A3, NAT_1:13;
then A6: k - 1 < (((len M) * (width M)) + 1) - 1 by XREAL_1:11;
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 A1, A4, A6, Th1;
then l div (width M) < len M by A4, NAT_D:18;
then A7: (l div (width M)) + 1 <= len M by NAT_1:13;
l mod (width M) < width M by A5, NAT_D:1;
then A8: (l mod (width M)) + 1 <= width M by NAT_1:13;
A9: ( (l div (width M)) + 1 >= 1 & (l mod (width M)) + 1 >= 1 ) by NAT_1:11;
then A10: (l div (width M)) + 1 in Seg (len M) by A7, FINSEQ_1:3;
A11: (l mod (width M)) + 1 in Seg (width M) by A8, A9, FINSEQ_1:3;
A12: l = ((l div (width M)) * (width M)) + (l mod (width M)) by A5, NAT_D:2;
thus [((l div (width M)) + 1),((l mod (width M)) + 1)] in Indices M by A10, A11, MATRPROB:12; :: thesis:
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 A1, A12 ;
hence (Mx2FinS M) . k = M * ((l div (width M)) + 1),((l mod (width M)) + 1) ; :: thesis: