theorem Th119: :: MATRIX13:119

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 & lines M is linearly-independent holds
lines (Segm (M,P,(Seg n))) is linearly-independent