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 qq = Mx2FinS (Infor_FinSeq_of M);
set pp = Infor_FinSeq_of p;
set MM = Infor_FinSeq_of M;
A1:
len p = (len M) * (width M)
by Th39;
A2:
len (Infor_FinSeq_of p) = len p
by Th47;
A3:
( len (Infor_FinSeq_of M) = len M & width (Infor_FinSeq_of M) = width M )
by Def8;
then
len (Mx2FinS (Infor_FinSeq_of M)) = (len M) * (width M)
by Th39;
then A4:
( dom (Mx2FinS (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of p) & dom (Mx2FinS (Infor_FinSeq_of M)) = dom p )
by A1, A2, FINSEQ_3:31;
now 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 A5:
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 A5, FINSEQ_1:def 3;
then
(
k >= 1 &
k <= len (Mx2FinS (Infor_FinSeq_of M)) )
by FINSEQ_1:3;
then reconsider l =
k - 1 as
Element of
NAT by NAT_1:21;
set ii =
(l div (width (Infor_FinSeq_of M))) + 1;
set jj =
(l mod (width (Infor_FinSeq_of M))) + 1;
A6:
(
[((l div (width (Infor_FinSeq_of M))) + 1),((l mod (width (Infor_FinSeq_of M))) + 1)] in Indices (Infor_FinSeq_of M) &
(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 A5, Th41;
A7:
p . k = M * ((l div (width (Infor_FinSeq_of M))) + 1),
((l mod (width (Infor_FinSeq_of M))) + 1)
by A3, A4, A5, Th41;
thus (Infor_FinSeq_of p) . k =
(p . k) * (log 2,(p . k))
by A4, A5, Th47
.=
(Mx2FinS (Infor_FinSeq_of M)) . k
by A6, A7, Th54
;
:: thesis: verum end;
hence
Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M)
by A4, FINSEQ_1:17; :: thesis: verum