theorem Th120: :: MATRIX13:120

for m, n being Nat
for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m & M is without_repeated_line holds
Segm (M,P,(Seg n)) is without_repeated_line