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) )
assume A1: 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:110;
set FG = F + G;
set Cf = ColVec2Mx f;
set Cg = ColVec2Mx g;
set Cfg = ColVec2Mx (F + G);
A2: ( len (F + G) = len f & len (ColVec2Mx (F + G)) = len (F + G) & len (ColVec2Mx f) = len f & len (ColVec2Mx g) = len f & len ((ColVec2Mx f) + (ColVec2Mx g)) = len (ColVec2Mx f) & width ((ColVec2Mx f) + (ColVec2Mx g)) = width (ColVec2Mx f) ) by A1, FINSEQ_1:def 18, MATRIX_1:def 3, MATRIX_3:def 3;

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

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

then ( (ColVec2Mx f) + (ColVec2Mx g) = {} & ColVec2Mx (F + G) = {} ) by A2;
hence (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g) ; :: thesis: verum

end;

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

then A4: ( len f in Seg (len f) & dom (ColVec2Mx f) = Seg (len f) & 1 in Seg 1 & width (ColVec2Mx f) = 1 & width (ColVec2Mx g) = 1 ) by A1, A2, FINSEQ_1:5, FINSEQ_1:def 3, MATRIX_1:24;
then [(len f),1] in Indices (ColVec2Mx f) by ZFMISC_1:106;
then Col ((ColVec2Mx f) + (ColVec2Mx g)),1 = (Col (ColVec2Mx f),1) + (Col (ColVec2Mx g),1) by A2, A4, MATRIX_4:60
.= f + (Col (ColVec2Mx g),1) by Th26, A3
.= f + g by Th26, A3, A1 ;
hence (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g) by Th26, A2, A4; :: thesis: verum

end;

end;