for m, n being Nat
for K being Field
for A being Matrix of n,m,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 holds
ex MVectors being Matrix of m -' n,m,K st
( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat
for M being Matrix of m,l,K st ( for i being Nat holds
( not i in Seg l or ex j being Nat st
( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) ) )