let x1, x2 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 & len x1 > 0 implies ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) )
assume that
A1: len x1 = len x2 and
A2: len x1 > 0 ; :: thesis: ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2)
A3: width (ColVec2Mx x1) = 1 by A2, Def9;
A4: Seg (width (ColVec2Mx x1)) = Seg 1 by A2, Def9;
A5: dom x1 = dom x2 by A1, FINSEQ_3:29;
A6: len (ColVec2Mx x1) = len x1 by A2, Def9;
then A7: dom (ColVec2Mx x1) = dom x1 by FINSEQ_3:29;
( len (ColVec2Mx x2) = len x2 & width (ColVec2Mx x2) = 1 ) by A1, A2, Def9;
then A8: Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1) by A1, A6, A3, MATRIX_4:55;
A9: len (x1 + x2) = len x1 by A1, RVSUM_1:115;
then A10: dom (x1 + x2) = dom x1 by FINSEQ_3:29;
A11: ( len (ColVec2Mx (x1 + x2)) = len (x1 + x2) & width (ColVec2Mx (x1 + x2)) = 1 ) by A2, A9, Def9;
then A12: Indices (ColVec2Mx (x1 + x2)) = Indices (ColVec2Mx x1) by A1, A6, A3, MATRIX_4:55, RVSUM_1:115;
for i, j being Nat st [i,j] in Indices (ColVec2Mx x1) holds
(ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) )
thus ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) ) :: thesis: verum

proof

assume A13: [i,j] in Indices (ColVec2Mx x1) ; :: thesis: (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j))
then consider q1 being FinSequence of REAL such that
A14: q1 = (ColVec2Mx x1) . i and
A15: (ColVec2Mx x1) * (i,j) = q1 . j by MATRIX_0:def 5;
j in Seg 1 by A4, A13, ZFMISC_1:87;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A16: j = 1 by XXREAL_0:1;
A17: i in dom x1 by A7, A13, ZFMISC_1:87;
then (ColVec2Mx x1) . i = <*(x1 . i)*> by A2, Def9;
then A18: q1 . j = x1 . i by A16, A14;
consider p being FinSequence of REAL such that
A19: p = (ColVec2Mx (x1 + x2)) . i and
A20: (ColVec2Mx (x1 + x2)) * (i,j) = p . j by A12, A13, MATRIX_0:def 5;
consider q2 being FinSequence of REAL such that
A21: q2 = (ColVec2Mx x2) . i and
A22: (ColVec2Mx x2) * (i,j) = q2 . j by A8, A13, MATRIX_0:def 5;
(ColVec2Mx x2) . i = <*(x2 . i)*> by A1, A2, A5, A17, Def9;
then A23: q2 . j = x2 . i by A16, A21;
(ColVec2Mx (x1 + x2)) . i = <*((x1 + x2) . i)*> by A2, A9, A10, A17, Def9;
then p . j = (x1 + x2) . i by A16, A19;
hence (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) by A10, A17, A20, A15, A18, A22, A23, VALUED_1:def 1; :: thesis: verum

end;

end;

hence ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) by A1, A6, A11, A3, Th26, RVSUM_1:115; :: thesis: verum