for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran (A,b1,b2)) iff v1 |-- b1 in Space_of_Solutions_of (A @) )