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))

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

hence
LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2)
by A1, A8, A4, Th26, RVSUM_1:115; :: thesis: verum
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;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