let K be Field; :: thesis: for f, g being FinSequence of K st len f = len g holds
(ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g)
let f, g be FinSequence of K; :: thesis: ( len f = len g implies (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g) )
set Cf = ColVec2Mx f;
set Cg = ColVec2Mx g;
A1: len (ColVec2Mx f) = len f by MATRIX_0:def 2;
assume A2: len f = len g ; :: thesis: (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g)
then reconsider F = f, G = g as Element of (len f) -tuples_on the carrier of K by FINSEQ_2:92;
A3: len (ColVec2Mx g) = len f by A2, MATRIX_0:def 2;
set FG = F + G;
set Cfg = ColVec2Mx (F + G);
A4: len (ColVec2Mx (F + G)) = len (F + G) by MATRIX_0:def 2;
A5: ( len (F + G) = len f & width ((ColVec2Mx f) + (ColVec2Mx g)) = width (ColVec2Mx f) ) by CARD_1:def 7, MATRIX_3:def 3;
A6: len ((ColVec2Mx f) + (ColVec2Mx g)) = len (ColVec2Mx f) by MATRIX_3:def 3;

per cases ( len f = 0 or len f > 0 ) ;

suppose A7: len f = 0 ; :: thesis: (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g)

then (ColVec2Mx f) + (ColVec2Mx g) = {} by A6, MATRIX_0:def 2;
hence (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g) by A4, A7; :: thesis: verum

end;

suppose A8: len f > 0 ; :: thesis: (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g)

then A10: width (ColVec2Mx f) = 1 by MATRIX_0:23;
then 1 in Seg (width (ColVec2Mx f)) ;
then Col (((ColVec2Mx f) + (ColVec2Mx g)),1) = (Col ((ColVec2Mx f),1)) + (Col ((ColVec2Mx g),1)) by A1, A3, MATRIX_4:60
.= f + (Col ((ColVec2Mx g),1)) by A8, Th26
.= f + g by A2, A8, Th26 ;
hence (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g) by A5, A8, A10, Th26; :: thesis: verum

end;

end;