theorem Th43: :: MATRIX15:43

for n being Nat
for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) ) holds
Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))