let M be m-nonnegative Matrix of REAL; 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 for k being Nat st k in dom (Mx2FinS (Infor_FinSeq_of M)) holds
(Infor_FinSeq_of p) . k = (Mx2FinS (Infor_FinSeq_of M)) . klet k be
Nat;
( 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))
;
(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
;
verum end;
hence
Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M)
by A4, FINSEQ_1:13; verum