for x being set
for k, m, n being Nat
for K being Field
for A being Matrix of n,k,K
for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds
x is Matrix of k,m,K