let k be Nat; :: thesis: for M being Matrix of k,F_Real holds
( Det M = 0. F_Real iff the_rank_of M < k )
let M be Matrix of k,F_Real; :: thesis: ( Det M = 0. F_Real iff the_rank_of M < k )
A1: ( Det M = 0. F_Real iff the_rank_of M <> k ) by MATRIX13:83;
A2: the_rank_of M <= len M by MATRIX13:74;
len M = k by MATRIX_0:def 2;
hence ( Det M = 0. F_Real iff the_rank_of M < k ) by A1, A2, XXREAL_0:1; :: thesis: verum