for n being Nat
for K being Field
for A being Matrix of n,n,K
for B being Matrix of K st Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)