theorem Th53: :: ENTROPY1:53

for M being m-nonnegative Matrix of REAL
for k being Nat st k in dom M holds
Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k))