let M be m-nonnegative Matrix of REAL; :: thesis: Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M)
reconsider p = Mx2FinS M as nonnegative FinSequence of REAL by Th43;
set pp = Infor_FinSeq_of p;
set qq = Mx2FinS (Infor_FinSeq_of M);
set MM = Infor_FinSeq_of M;
A1: len p = (len M) * (width M) by Th39;
A2: width (Infor_FinSeq_of M) = width M by Def8;
len (Infor_FinSeq_of M) = len M by Def8;
then A3: len (Mx2FinS (Infor_FinSeq_of M)) = (len M) * (width M) by A2, Th39;
len (Infor_FinSeq_of p) = len p by Th47;
then A4: dom (Mx2FinS (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of p) by A1, A3, FINSEQ_3:29;
A5: dom (Mx2FinS (Infor_FinSeq_of M)) = dom p by A1, A3, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom (Mx2FinS (Infor_FinSeq_of M)) holds
(Infor_FinSeq_of p) . k = (Mx2FinS (Infor_FinSeq_of M)) . k

let k be Nat; :: thesis: ( k in dom (Mx2FinS (Infor_FinSeq_of M)) implies (Infor_FinSeq_of p) . k = (Mx2FinS (Infor_FinSeq_of M)) . k )
assume A6: k in dom (Mx2FinS (Infor_FinSeq_of M)) ; :: thesis: (Infor_FinSeq_of p) . k = (Mx2FinS (Infor_FinSeq_of M)) . k
k in Seg (len (Mx2FinS (Infor_FinSeq_of M))) by A6, FINSEQ_1:def 3;
then k >= 1 by FINSEQ_1:1;
then reconsider l = k - 1 as Nat by NAT_1:21;
set jj = (l mod (width (Infor_FinSeq_of M))) + 1;
set ii = (l div (width (Infor_FinSeq_of M))) + 1;
A7: [((l div (width (Infor_FinSeq_of M))) + 1),((l mod (width (Infor_FinSeq_of M))) + 1)] in Indices (Infor_FinSeq_of M) by A6, Th41;
A8: (Mx2FinS (Infor_FinSeq_of M)) . k = (Infor_FinSeq_of M) * (((l div (width (Infor_FinSeq_of M))) + 1),((l mod (width (Infor_FinSeq_of M))) + 1)) by A6, Th41;
A9: p . k = M * (((l div (width (Infor_FinSeq_of M))) + 1),((l mod (width (Infor_FinSeq_of M))) + 1)) by A2, A5, A6, Th41;
thus (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) by A4, A6, Th47
.= (Mx2FinS (Infor_FinSeq_of M)) . k by A7, A8, A9, Th54 ; :: thesis: verum

end;

hence Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M) by A4, FINSEQ_1:13; :: thesis: verum