theorem Th113: :: MATRIX13:113

for m, n being Nat
for K being Field
for M being Matrix of m,n,K
for i being Nat
for a being Element of K st ( for j being Nat st j in Seg m holds
M * (j,i) = a ) holds
( M is without_repeated_line iff Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) is without_repeated_line )