for k being Nat
for M being Matrix of k,F_Real holds
( Det M = 0. F_Real iff the_rank_of M < k )