let k be Nat; :: thesis: for M being Matrix of k,F_Real holds
( ( lines M is linearly-dependent or not M is without_repeated_line ) iff the_rank_of M < k )
let M be Matrix of k,F_Real; :: thesis: ( ( lines M is linearly-dependent or not M is without_repeated_line ) iff the_rank_of M < k )
A1: ( the_rank_of M = k iff ( lines M is linearly-independent & M is without_repeated_line ) ) by MATRIX13:121;
A2: the_rank_of M <= len M by MATRIX13:74;
len M = k by MATRIX_0:def 2;
hence ( ( lines M is linearly-dependent or not M is without_repeated_line ) iff the_rank_of M < k ) by A1, A2, XXREAL_0:1; :: thesis: verum