let n be Nat; :: thesis: for M being Matrix of n,F_Rat st M is without_repeated_line holds
( Det M <> 0. F_Rat iff lines M is linearly-independent )
let M be Matrix of n,F_Rat; :: thesis: ( M is without_repeated_line implies ( Det M <> 0. F_Rat iff lines M is linearly-independent ) )
assume AS: M is without_repeated_line ; :: thesis: ( Det M <> 0. F_Rat iff lines M is linearly-independent )
hereby :: thesis: ( lines M is linearly-independent implies Det M <> 0. F_Rat )
assume Det M <> 0. F_Rat ; :: thesis: lines M is linearly-independent
then the_rank_of M = n by MATRIX13:83;
hence lines M is linearly-independent by MATRIX13:110; :: thesis: verum
end;
assume lines M is linearly-independent ; :: thesis: Det M <> 0. F_Rat
then the_rank_of M = n by AS, MATRIX13:121;
hence Det M <> 0. F_Rat by MATRIX13:83; :: thesis: verum