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_1:def 3;
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:110;
A3: len (ColVec2Mx g) = len f by A2, MATRIX_1:def 3;
set FG = F + G;
set Cfg = ColVec2Mx (F + G);
A4: len (ColVec2Mx (F + G)) = len (F + G) by MATRIX_1:def 3;
A5: ( len (F + G) = len f & width ((ColVec2Mx f) + (ColVec2Mx g)) = width (ColVec2Mx f) ) by FINSEQ_1:def 18, 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_1:def 3;
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)

A9: ( dom (ColVec2Mx f) = Seg (len f) & 1 in Seg 1 ) by A1, FINSEQ_1:def 3;
A10: width (ColVec2Mx f) = 1 by A8, MATRIX_1:24;
len f in Seg (len f) by A8, FINSEQ_1:5;
then [(len f),1] in Indices (ColVec2Mx f) by A9, A10, ZFMISC_1:106;
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;