theorem :: MATRIX15:27

for K being Field
for f, g being FinSequence of K st len f = len g holds
(LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)