theorem Th23: :: MATRIXR2:23
for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)