:: deftheorem defines Solutions_of MATRIX15:def 4 :
for K being Field
for A being Matrix of K
for b being FinSequence of K holds Solutions_of (A,b) = { f where f is FinSequence of K : ColVec2Mx f in Solutions_of (A,(ColVec2Mx b)) } ;