for x1, x2 being FinSequence of REAL st len x1 = len x2 & len x1 > 0 holds
ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2)