theorem Th45: :: MATRIX15:45

for K being Field
for A, B being Matrix of K
for N being finite without_zero Subset of NAT st N c= dom A & not N is empty & dom A = dom B & ( for i being Nat st i in (dom A) \ N holds
( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds
Solutions_of (A,B) = Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B)))))