let K be Field; :: thesis: for f, g being FinSequence of K st len f = len g holds
() + () = ColVec2Mx (f + g)

let f, g be FinSequence of K; :: thesis: ( len f = len g implies () + () = ColVec2Mx (f + g) )
set Cf = ColVec2Mx f;
set Cg = ColVec2Mx g;
A1: len () = len f by MATRIX_0:def 2;
assume A2: len f = len g ; :: thesis: () + () = 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 () = len f by ;
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 (() + ()) = width () ) by ;
A6: len (() + ()) = len () by MATRIX_3:def 3;
per cases ( len f = 0 or len f > 0 ) ;
suppose A7: len f = 0 ; :: thesis: () + () = ColVec2Mx (f + g)
then (ColVec2Mx f) + () = {} by ;
hence (ColVec2Mx f) + () = ColVec2Mx (f + g) by A4, A7; :: thesis: verum
end;
suppose A8: len f > 0 ; :: thesis: () + () = ColVec2Mx (f + g)
A9: ( dom () = Seg (len f) & 1 in Seg 1 ) by ;
A10: width () = 1 by ;
len f in Seg (len f) by ;
then [(len f),1] in Indices () by ;
then Col ((() + ()),1) = (Col ((),1)) + (Col ((),1)) by
.= f + (Col ((),1)) by
.= f + g by A2, A8, Th26 ;
hence (ColVec2Mx f) + () = ColVec2Mx (f + g) by A5, A8, A10, Th26; :: thesis: verum
end;
end;