theorem Th114: :: MATRIX13:114

for m, n being Nat
for K being Field
for M being Matrix of m,n,K
for i being Nat st M is without_repeated_line & lines M is linearly-independent & ( for j being Nat st j in Seg m holds
M * (j,i) = 0. K ) holds
lines (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) is linearly-independent