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

end;

hence LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2) by A4, A8, A10, A1, A6, Th22; :: thesis: verum