for n, m being Nat
for M being Matrix of n,m,F_Real holds
( Mx2Tran M is onto iff the_rank_of M = m )