theorem Th39: :: MATRTOP1:39

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