theorem :: ZMODLAT2:60

for n being Nat
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 )