let K be Field; :: thesis: for f, g being FinSequence of K st len f = len g holds
(LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)
let f, g be FinSequence of K; :: thesis: ( len f = len g implies (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g) )
set Lf = LineVec2Mx f;
set Lg = LineVec2Mx g;
A1: len (LineVec2Mx f) = 1 by CARD_1:def 7;
assume A2: len f = len g ; :: thesis: (LineVec2Mx f) + (LineVec2Mx g) = 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 (LineVec2Mx g) = len f by A2, MATRIX_0:23;
set FG = F + G;
set Lfg = LineVec2Mx (F + G);
A6: len ((LineVec2Mx f) + (LineVec2Mx g)) = len (LineVec2Mx f) by MATRIX_3:def 3;
( dom (LineVec2Mx f) = Seg 1 & 1 in Seg 1 ) by A1, FINSEQ_1:def 3;
then 1 in dom (LineVec2Mx f) ;
then Line (((LineVec2Mx f) + (LineVec2Mx g)),1) = (Line ((LineVec2Mx f),1)) + (Line ((LineVec2Mx g),1)) by A3, MATRIX_0:23, MATRIX_4:59
.= f + (Line ((LineVec2Mx g),1)) by Th25
.= f + g by Th25 ;
hence (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g) by A1, A6, Th25; :: thesis: verum