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, MATRIXR1:def 9;
A4: Seg (width (ColVec2Mx x1)) = Seg 1 by A2, MATRIXR1:def 9;
A5: dom x1 = dom x2 by A1, FINSEQ_3:29;
A6: len (x1 - x2) = len x1 by A1, RVSUM_1:116;
then A7: dom (x1 - x2) = dom x1 by FINSEQ_3:29;
A8: len (ColVec2Mx x1) = len x1 by A2, MATRIXR1:def 9;
then A9: dom (ColVec2Mx x1) = dom x1 by FINSEQ_3:29;
A10: ( len (ColVec2Mx x2) = len x2 & width (ColVec2Mx x2) = 1 ) by A1, A2, MATRIXR1:def 9;
then A11: Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1) by A1, A8, A3, MATRIX_4:55;
A12: ( len (ColVec2Mx (x1 - x2)) = len (x1 - x2) & width (ColVec2Mx (x1 - x2)) = 1 ) by A2, A6, MATRIXR1:def 9;
then A13: Indices (ColVec2Mx (x1 - x2)) = Indices (ColVec2Mx x1) by A1, A8, A3, MATRIX_4:55, RVSUM_1:116;
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)) )
assume A14: [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
A15: q1 = (ColVec2Mx x1) . i and
A16: (ColVec2Mx x1) * (i,j) = q1 . j by MATRIX_0:def 5;
j in Seg 1 by A4, A14, ZFMISC_1:87;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A17: j = 1 by XXREAL_0:1;
A18: i in dom x1 by A9, A14, ZFMISC_1:87;
then (ColVec2Mx x1) . i = <*(x1 . i)*> by A2, MATRIXR1:def 9;
then A19: q1 . j = x1 . i by A17, A15;
consider p being FinSequence of REAL such that
A20: p = (ColVec2Mx (x1 - x2)) . i and
A21: (ColVec2Mx (x1 - x2)) * (i,j) = p . j by A13, A14, MATRIX_0:def 5;
consider q2 being FinSequence of REAL such that
A22: q2 = (ColVec2Mx x2) . i and
A23: (ColVec2Mx x2) * (i,j) = q2 . j by A11, A14, MATRIX_0:def 5;
(ColVec2Mx x2) . i = <*(x2 . i)*> by A1, A2, A5, A18, MATRIXR1:def 9;
then A24: q2 . j = x2 . i by A17, A22;
(ColVec2Mx (x1 - x2)) . i = <*((x1 - x2) . i)*> by A2, A6, A7, A18, MATRIXR1:def 9;
then p . j = (x1 - x2) . i by A17, A20;
hence (ColVec2Mx (x1 - x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) - ((ColVec2Mx x2) * (i,j)) by A1, A21, A16, A19, A23, A24, Lm1; :: thesis: verum

end;

hence ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2) by A1, A6, A8, A12, A3, A10, Th22; :: thesis: verum