theorem :: MATRIX15:34

for i being Nat
for K being Field
for A, B, X being Matrix of K st X in Solutions_of (A,B) & i in Seg (width X) & Col (X,i) = (len X) |-> (0. K) holds
Col (B,i) = (len B) |-> (0. K)