for M being m-nonnegative Matrix of REAL holds Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M)