let M be m-nonnegative Matrix of REAL; :: thesis: for M1 being Matrix of REAL holds
( M1 = Infor_FinSeq_of M iff ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j)))) ) ) )
let M1 be Matrix of REAL; :: thesis: ( M1 = Infor_FinSeq_of M iff ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j)))) ) ) )

hereby :: thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j)))) ) implies M1 = Infor_FinSeq_of M )

assume A1: M1 = Infor_FinSeq_of M ; :: thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j)))) ) )
then A2: width M1 = width M by Def8;
A3: len M1 = len M by A1, Def8;

now :: thesis: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j))))

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j)))) )
assume A4: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j))))
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_0:def 7;
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_0:def 7;
thus M1 * (i,j) = (Line (M1,i)) . j by A5, MATRIX_0:def 7
.= (Infor_FinSeq_of p) . j by A1, A6, Th53
.= (M * (i,j)) * (log (2,(M * (i,j)))) by A9, A8, Th47 ; :: thesis: verum

end;

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

end;

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

proof

let k be Nat; :: thesis: ( k in dom M1 implies M1 . k = mlt ((Line (M,k)),(FinSeq_log (2,(Line (M,k))))) )
assume A14: k in dom M1 ; :: thesis: M1 . k = mlt ((Line (M,k)),(FinSeq_log (2,(Line (M,k)))))
A15: len (M1 . k) = width M1 by A14, MATRIX_0:36;
reconsider p = Line (M,k) as nonnegative FinSequence of REAL by A13, A14, Th19;
A16: len p = width M by MATRIX_0:def 7;
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:29;
A19: k in Seg (len M) by A10, A14, FINSEQ_1:def 3;

now :: thesis: for j being Nat st j in dom (M1 . k) holds
(M1 . k) . j = (mlt (p,(FinSeq_log (2,p)))) . j

let j be Nat; :: thesis: ( j in dom (M1 . k) implies (M1 . k) . b₁ = (mlt (p,(FinSeq_log (2,p)))) . b₁ )
assume A20: j in dom (M1 . k) ; :: thesis: (M1 . k) . b₁ = (mlt (p,(FinSeq_log (2,p)))) . b₁
A21: j in Seg (width M) by A11, A15, A20, FINSEQ_1:def 3;
then A22: p . j = M * (k,j) by MATRIX_0:def 7;
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 RVSUM_1:59
.= (M * (k,j)) * ((FinSeq_log (2,p)) . j) by A21, MATRIX_0:def 7 ;
A25: j in dom (FinSeq_log (2,p)) by A16, A17, A21, FINSEQ_1:def 3;
A26: [k,j] in Indices M1 by A14, A20, MATRPROB:13;
then A27: (M1 . k) . j = M1 * (k,j) by MATRPROB:14
.= (M * (k,j)) * (log (2,(M * (k,j)))) by A12, A26 ;

per cases ( M * (k,j) = 0 or M * (k,j) > 0 ) by A23, MATRPROB:def 6;

suppose M * (k,j) = 0 ; :: thesis: (M1 . k) . b₁ = (mlt (p,(FinSeq_log (2,p)))) . b₁

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

end;

suppose M * (k,j) > 0 ; :: thesis: (mlt (p,(FinSeq_log (2,p)))) . b₁ = (M1 . k) . b₁

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

end;

end;

end;

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

end;

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