let M be m-nonnegative Matrix of REAL ; :: thesis:
let M1 be Matrix of REAL ; :: thesis:

hereby :: thesis:

assume A1: M1 = Infor_FinSeq_of M ; :: thesis:
then A2: width M1 = width M by Def8;
A3: len M1 = len M by A1, Def8;

now

let i, j be Element of NAT ; :: thesis:
assume A4: [i,j] in Indices M1 ; :: thesis:
A5: j in Seg (width M1) by A4, MATRPROB:12;
i in Seg (len M1) by A4, MATRPROB:12;
then A6: i in dom M by A3, FINSEQ_1:def 3;
then reconsider p = Line M,i as nonnegative FinSequence of REAL by Th19;
A7: len p = width M by MATRIX_1:def 8;
len p = len (Infor_FinSeq_of p) by Th47;
then A8: j in dom (Infor_FinSeq_of p) by A2, A5, A7, FINSEQ_1:def 3;
A9: p . j = M * i,j by A2, A5, MATRIX_1:def 8;
thus M1 * i,j = (Line M1,i) . j by A5, MATRIX_1:def 8
.= (Infor_FinSeq_of p) . j by A1, A6, Th53
.= (M * i,j) * (log 2,(M * i,j)) by A9, A8, Th47 ; :: thesis:

end;

hence ( len M1 = len M & width M1 = width M & ( for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * i,j = (M * i,j) * (log 2,(M * i,j)) ) ) by A1, Def8; :: thesis:

end;

assume that
A10: len M1 = len M and
A11: width M1 = width M and
A12: for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * i,j = (M * i,j) * (log 2,(M * i,j)) ; :: thesis:
A13: dom M1 = dom M by A10, FINSEQ_3:31;
for k being Element of NAT st k in dom M1 holds
M1 . k = mlt (Line M,k),(FinSeq_log 2,(Line M,k))

proof

let k be Element of NAT ; :: thesis:
assume A14: k in dom M1 ; :: thesis:
A15: len (M1 . k) = width M1 by A14, GOBRD13:4;
reconsider p = Line M,k as nonnegative FinSequence of REAL by A13, A14, Th19;
A16: len p = width M by MATRIX_1:def 8;
A17: len (FinSeq_log 2,p) = len p by Def6;
then len (mlt p,(FinSeq_log 2,p)) = len p by MATRPROB:30;
then A18: dom (M1 . k) = dom (mlt p,(FinSeq_log 2,p)) by A11, A16, A15, FINSEQ_3:31;
A19: k in Seg (len M) by A10, A14, FINSEQ_1:def 3;

now

let j be Nat; :: thesis:
assume A20: j in dom (M1 . k) ; :: thesis:
A21: j in Seg (width M) by A11, A15, A20, FINSEQ_1:def 3;
then A22: p . j = M * k,j by MATRIX_1:def 8;
A23: [k,j] in Indices M by A19, A21, MATRPROB:12;
A24: (mlt p,(FinSeq_log 2,p)) . j = (p . j) * ((FinSeq_log 2,p) . j) by A18, A20, RVSUM_1:86
.= (M * k,j) * ((FinSeq_log 2,p) . j) by A21, MATRIX_1:def 8 ;
A25: j in dom (FinSeq_log 2,p) by A16, A17, A21, FINSEQ_1:def 3;
A26: j in NAT by ORDINAL1:def 13;
A27: [k,j] in Indices M1 by A14, A20, MATRPROB:13;
then A28: (M1 . k) . j = M1 * k,j by A26, MATRPROB:14
.= (M * k,j) * (log 2,(M * k,j)) by A12, A26, A27 ;

per cases by A26, A23, MATRPROB:def 6;

suppose M * k,j = 0 ; :: thesis:

hence (M1 . k) . j = (mlt p,(FinSeq_log 2,p)) . j by A28, A24; :: thesis:

end;

suppose M * k,j > 0 ; :: thesis:

hence (mlt p,(FinSeq_log 2,p)) . j = (M1 . k) . j by A25, A28, A22, A24, Def6; :: thesis:

end;

end;

end;

hence M1 . k = mlt (Line M,k),(FinSeq_log 2,(Line M,k)) by A18, FINSEQ_1:17; :: thesis:

end;

hence M1 = Infor_FinSeq_of M by A10, A11, Def8; :: thesis: