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

let f, g be FinSequence of K; :: thesis: ( len f = len g implies () + () = LineVec2Mx (f + g) )
set Lf = LineVec2Mx f;
set Lg = LineVec2Mx g;
A1: len () = 1 by CARD_1:def 7;
assume A2: len f = len g ; :: thesis: () + () = LineVec2Mx (f + g)
then reconsider F = f, G = g as Element of (len f) -tuples_on the carrier of K by FINSEQ_2:92;
A3: width () = len f by ;
set FG = F + G;
set Lfg = LineVec2Mx (F + G);
A4: ( len (F + G) = len f & len (LineVec2Mx (F + G)) = 1 ) by CARD_1:def 7;
A5: width (LineVec2Mx (F + G)) = len (F + G) by MATRIX_0:23;
A6: len (() + ()) = len () by MATRIX_3:def 3;
A7: width (() + ()) = width () by MATRIX_3:def 3;
A8: width () = len f by MATRIX_0:23;
per cases ( len f = 0 or len f > 0 ) ;
suppose len f = 0 ; :: thesis: () + () = LineVec2Mx (f + g)
then Seg (len f) = {} ;
then for i, j being Nat st [i,j] in Indices (() + ()) holds
(() + ()) * (i,j) = (LineVec2Mx (F + G)) * (i,j) by ;
hence (LineVec2Mx f) + () = LineVec2Mx (f + g) by A4, A1, A6, A7, A8, A5, MATRIX_0:21; :: thesis: verum
end;
suppose A9: len f > 0 ; :: thesis: () + () = LineVec2Mx (f + g)
A10: ( dom () = Seg 1 & 1 in Seg 1 ) by ;
len f in Seg (len f) by ;
then [1,(len f)] in Indices () by ;
then Line ((() + ()),1) = (Line ((),1)) + (Line ((),1)) by
.= f + (Line ((),1)) by Th25
.= f + g by Th25 ;
hence (LineVec2Mx f) + () = LineVec2Mx (f + g) by A1, A6, Th25; :: thesis: verum
end;
end;