theorem Th28: :: MATRIX15:28

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