for m being Nat st 0 < m holds
for M being Matrix of m,1,F_Real holds M is FinSequence of 1 -tuples_on REAL