theorem Th109: :: MATRIX13:109

for m, n being Nat
for K being Field
for M being Matrix of m,n,K st M is without_repeated_line holds
( ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent )