let x1, x2 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 & len x1 > 0 implies LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) )
assume A1: ( len x1 = len x2 & len x1 > 0 ) ; :: thesis: LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2)
then A2: len (x1 + x2) = len x1 by EUCLID_2:6;
A3: dom x1 = dom x2 by A1, FINSEQ_3:31;
A4: width (LineVec2Mx (x1 + x2)) = len (x1 + x2) by Def10;
A5: width (LineVec2Mx x1) = len x1 by Def10;
A6: width (LineVec2Mx x2) = len x2 by Def10;
A7: dom (x1 + x2) = dom x1 by A2, FINSEQ_3:31;
A8: len (LineVec2Mx (x1 + x2)) = 1 by Def10;
A9: len (LineVec2Mx x1) = 1 by Def10;
A10: len (LineVec2Mx x2) = 1 by Def10;
A11: Indices (LineVec2Mx (x1 + x2)) = Indices (LineVec2Mx x1) by A1, A4, A5, A8, A9, EUCLID_2:6, MATRIX_4:55;
A12: Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1) by A1, A5, A6, A9, A10, MATRIX_4:55;
A13: dom (LineVec2Mx x1) = Seg (len (LineVec2Mx x1)) by FINSEQ_1:def 3
.= Seg 1 by Def10 ;
A14: Seg (width (LineVec2Mx x1)) = Seg (len x1) by Def10
.= dom x1 by FINSEQ_1:def 3 ;
for i, j being Nat st [i,j] in Indices (LineVec2Mx x1) holds
(LineVec2Mx (x1 + x2)) * i,j = ((LineVec2Mx x1) * i,j) + ((LineVec2Mx x2) * i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (LineVec2Mx x1) implies (LineVec2Mx (x1 + x2)) * i,j = ((LineVec2Mx x1) * i,j) + ((LineVec2Mx x2) * i,j) )
assume A15: [i,j] in Indices (LineVec2Mx x1) ; :: thesis: (LineVec2Mx (x1 + x2)) * i,j = ((LineVec2Mx x1) * i,j) + ((LineVec2Mx x2) * i,j)
then A16: ( i in Seg 1 & j in dom x1 ) by A13, A14, ZFMISC_1:106;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:3;
then A17: i = 1 by XXREAL_0:1;
consider p being FinSequence of REAL such that
A18: ( p = (LineVec2Mx (x1 + x2)) . i & (LineVec2Mx (x1 + x2)) * i,j = p . j ) by A11, A15, MATRIX_1:def 6;
A19: p . j = (x1 + x2) . j by A7, A16, A17, A18, Def10;
consider q1 being FinSequence of REAL such that
A20: ( q1 = (LineVec2Mx x1) . i & (LineVec2Mx x1) * i,j = q1 . j ) by A15, MATRIX_1:def 6;
A21: q1 . j = x1 . j by A16, A17, A20, Def10;
consider q2 being FinSequence of REAL such that
A22: ( q2 = (LineVec2Mx x2) . i & (LineVec2Mx x2) * i,j = q2 . j ) by A12, A15, MATRIX_1:def 6;
q2 . j = x2 . j by A3, A16, A17, A22, Def10;
hence (LineVec2Mx (x1 + x2)) * i,j = ((LineVec2Mx x1) * i,j) + ((LineVec2Mx x2) * i,j) by A7, A16, A18, A19, A20, A21, A22, VALUED_1:def 1; :: thesis: verum

end;

hence LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) by A1, A2, A4, A5, A6, A8, A9, A10, Th26; :: thesis: verum