theorem :: MATRIXR1:48
for x being FinSequence of REAL
for M being Matrix of REAL holds
( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )