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 )

then the_rank_of M = n by AS, MATRIX13:121;

hence Det M <> 0. F_Rat by MATRIX13:83; :: thesis: verum

( 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
lines M is linearly-independent
; :: thesis: Det M <> 0. F_Ratassume
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;then the_rank_of M = n by MATRIX13:83;

hence lines M is linearly-independent by MATRIX13:110; :: thesis: verum

then the_rank_of M = n by AS, MATRIX13:121;

hence Det M <> 0. F_Rat by MATRIX13:83; :: thesis: verum