for K being Field
for a being Element of K
for A, B, X being Matrix of K st X in Solutions_of (A,B) holds
( a * X in Solutions_of (A,(a * B)) & X in Solutions_of ((a * A),(a * B)) )