theorem :: MATRIX15:48

for k, m, n being Nat
for K being Field
for A being Matrix of n,m,K
for B being Matrix of n,k,K
for P being Function of (Seg n),(Seg n) holds
( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )