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);

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 ((LineVec2Mx f) + (LineVec2Mx g)) = len (LineVec2Mx f) by MATRIX_3:def 3;

A7: width ((LineVec2Mx f) + (LineVec2Mx g)) = width (LineVec2Mx f) by MATRIX_3:def 3;

A8: width (LineVec2Mx f) = len f by MATRIX_0:23;

(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);

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 ((LineVec2Mx f) + (LineVec2Mx g)) = len (LineVec2Mx f) by MATRIX_3:def 3;

A7: width ((LineVec2Mx f) + (LineVec2Mx g)) = width (LineVec2Mx f) by MATRIX_3:def 3;

A8: width (LineVec2Mx f) = len f by MATRIX_0:23;

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

end;

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

then
Seg (len f) = {}
;

then for i, j being Nat st [i,j] in Indices ((LineVec2Mx f) + (LineVec2Mx g)) holds

((LineVec2Mx f) + (LineVec2Mx g)) * (i,j) = (LineVec2Mx (F + G)) * (i,j) by A7, A8, ZFMISC_1:90;

hence (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g) by A4, A1, A6, A7, A8, A5, MATRIX_0:21; :: thesis: verum

end;then for i, j being Nat st [i,j] in Indices ((LineVec2Mx f) + (LineVec2Mx g)) holds

((LineVec2Mx f) + (LineVec2Mx g)) * (i,j) = (LineVec2Mx (F + G)) * (i,j) by A7, A8, ZFMISC_1:90;

hence (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g) by A4, A1, A6, A7, A8, A5, MATRIX_0:21; :: thesis: verum

suppose A9:
len f > 0
; :: thesis: (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)

A10:
( dom (LineVec2Mx f) = Seg 1 & 1 in Seg 1 )
by A1, FINSEQ_1:def 3;

len f in Seg (len f) by A9, FINSEQ_1:3;

then [1,(len f)] in Indices (LineVec2Mx f) by A8, A10, ZFMISC_1:87;

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

end;len f in Seg (len f) by A9, FINSEQ_1:3;

then [1,(len f)] in Indices (LineVec2Mx f) by A8, A10, ZFMISC_1:87;

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