theorem :: MATRIX15:47
for K being Field
for A, B being Matrix of K
for i being Nat st i in dom A & len A > 1 & Line (A,i) = (width A) |-> (0. K) & i in dom B & Line (B,i) = (width B) |-> (0. K) holds
Solutions_of (A,B) = Solutions_of ((DelLine (A,i)),(DelLine (B,i)))