let x1, x2 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 & len x1 > 0 implies ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2) )
assume A1: ( len x1 = len x2 & len x1 > 0 ) ; :: thesis: ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2)
then A2: len (x1 - x2) = len x1 by EUCLID_2:7;
then A3: len (ColVec2Mx (x1 - x2)) = len (x1 - x2) by A1, MATRIXR1:def 9;
A4: dom x1 = dom x2 by A1, FINSEQ_3:31;
A5: len (ColVec2Mx x1) = len x1 by A1, MATRIXR1:def 9;
A6: len (ColVec2Mx x2) = len x2 by A1, MATRIXR1:def 9;
A7: dom (x1 - x2) = dom x1 by A2, FINSEQ_3:31;
A8: width (ColVec2Mx (x1 - x2)) = 1 by A1, A2, MATRIXR1:def 9;
A9: width (ColVec2Mx x1) = 1 by A1, MATRIXR1:def 9;
A10: width (ColVec2Mx x2) = 1 by A1, MATRIXR1:def 9;
A11: Indices (ColVec2Mx (x1 - x2)) = Indices (ColVec2Mx x1) by A1, A3, A5, A8, A9, EUCLID_2:7, MATRIX_4:55;
A12: Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1) by A1, A5, A6, A9, A10, MATRIX_4:55;
A13: dom (ColVec2Mx x1) = dom x1 by A5, FINSEQ_3:31;
A14: Seg (width (ColVec2Mx x1)) = Seg 1 by A1, MATRIXR1:def 9;
for i, j being Element of 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 Element of NAT ; :: thesis: ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 - x2)) * i,j = ((ColVec2Mx x1) * i,j) - ((ColVec2Mx x2) * i,j) )
assume A15: [i,j] in Indices (ColVec2Mx x1) ; :: thesis: (ColVec2Mx (x1 - x2)) * i,j = ((ColVec2Mx x1) * i,j) - ((ColVec2Mx x2) * i,j)
then A16: ( i in dom x1 & j in Seg 1 ) by A13, A14, ZFMISC_1:106;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:3;
then A17: j = 1 by XXREAL_0:1;
consider p being FinSequence of REAL such that
A18: ( p = (ColVec2Mx (x1 - x2)) . i & (ColVec2Mx (x1 - x2)) * i,j = p . j ) by A11, A15, MATRIX_1:def 6;
(ColVec2Mx (x1 - x2)) . i = <*((x1 - x2) . i)*> by A1, A2, A7, A16, MATRIXR1:def 9;
then A19: p . j = (x1 - x2) . i by A17, A18, FINSEQ_1:57;
consider q1 being FinSequence of REAL such that
A20: ( q1 = (ColVec2Mx x1) . i & (ColVec2Mx x1) * i,j = q1 . j ) by A15, MATRIX_1:def 6;
(ColVec2Mx x1) . i = <*(x1 . i)*> by A1, A16, MATRIXR1:def 9;
then A21: q1 . j = x1 . i by A17, A20, FINSEQ_1:57;
consider q2 being FinSequence of REAL such that
A22: ( q2 = (ColVec2Mx x2) . i & (ColVec2Mx x2) * i,j = q2 . j ) by A12, A15, MATRIX_1:def 6;
(ColVec2Mx x2) . i = <*(x2 . i)*> by A1, A4, A16, MATRIXR1:def 9;
then q2 . j = x2 . i by A17, A22, FINSEQ_1:57;
hence (ColVec2Mx (x1 - x2)) * i,j = ((ColVec2Mx x1) * i,j) - ((ColVec2Mx x2) * i,j) by A1, A18, A19, A20, A21, A22, Lm1; :: thesis: verum

end;

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