for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
ColVec2Mx (M2F p) = p