let x1, x2 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 implies LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) )
assume A1: len x1 = len x2 ; :: thesis: LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2)
then A2: dom x1 = dom x2 by FINSEQ_3:29;
len (x1 + x2) = len x1 by A1, RVSUM_1:115;
then A3: dom (x1 + x2) = dom x1 by FINSEQ_3:29;
A4: ( width (LineVec2Mx x1) = len x1 & len (LineVec2Mx x1) = 1 ) by Def10;
( width (LineVec2Mx x2) = len x2 & len (LineVec2Mx x2) = 1 ) by Def10;
then A5: Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1) by A1, A4, MATRIX_4:55;
A6: Seg (width (LineVec2Mx x1)) = Seg (len x1) by Def10
.= dom x1 by FINSEQ_1:def 3 ;
A7: dom (LineVec2Mx x1) = Seg (len (LineVec2Mx x1)) by FINSEQ_1:def 3
.= Seg 1 by Def10 ;
A8: ( width (LineVec2Mx (x1 + x2)) = len (x1 + x2) & len (LineVec2Mx (x1 + x2)) = 1 ) by Def10;
then A9: Indices (LineVec2Mx (x1 + x2)) = Indices (LineVec2Mx x1) by A1, A4, MATRIX_4:55, RVSUM_1:115;
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 A10: [i,j] in Indices (LineVec2Mx x1) ; :: thesis: (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j))
then consider q1 being FinSequence of REAL such that
q1 = (LineVec2Mx x1) . i and
A11: (LineVec2Mx x1) * (i,j) = q1 . j by MATRIX_0:def 5;
consider p being FinSequence of REAL such that
p = (LineVec2Mx (x1 + x2)) . i and
A12: (LineVec2Mx (x1 + x2)) * (i,j) = p . j by A9, A10, MATRIX_0:def 5;
consider q2 being FinSequence of REAL such that
q2 = (LineVec2Mx x2) . i and
A13: (LineVec2Mx x2) * (i,j) = q2 . j by A5, A10, MATRIX_0:def 5;
A14: j in dom x1 by A6, A10, ZFMISC_1:87;
i in Seg 1 by A7, A10, ZFMISC_1:87;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A15: i = 1 by XXREAL_0:1;
then A16: q1 . j = x1 . j by A14, A11, Def10;
A17: q2 . j = x2 . j by A2, A14, A15, A13, Def10;
p . j = (x1 + x2) . j by A3, A14, A15, A12, Def10;
hence (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) by A3, A14, A12, A11, A16, A13, A17, VALUED_1:def 1; :: thesis: verum

end;

hence LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) by A1, A8, A4, Th26, RVSUM_1:115; :: thesis: verum