let x1, x2 be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds

(x1 + x2) * A = (x1 * A) + (x2 * A)

let A be Matrix of REAL; :: thesis: ( len x1 = len x2 & len A = len x1 & len x1 > 0 implies (x1 + x2) * A = (x1 * A) + (x2 * A) )

assume that

A1: len x1 = len x2 and

A2: len A = len x1 and

A3: len x1 > 0 ; :: thesis: (x1 + x2) * A = (x1 * A) + (x2 * A)

A4: width (LineVec2Mx x2) = len x2 by Def10;

A5: width (LineVec2Mx x1) = len x1 by Def10;

then A6: width ((LineVec2Mx x1) * A) = width A by A2, MATRIX_3:def 4

.= width ((LineVec2Mx x2) * A) by A1, A2, A4, MATRIX_3:def 4 ;

A7: len (LineVec2Mx x1) = 1 by Def10;

then A8: 1 <= len ((LineVec2Mx x1) * A) by A2, A5, MATRIX_3:def 4;

A9: len (LineVec2Mx x2) = 1 by Def10;

thus (x1 + x2) * A = Line ((((LineVec2Mx x1) + (LineVec2Mx x2)) * A),1) by A1, Th50

.= Line ((((LineVec2Mx x1) * A) + ((LineVec2Mx x2) * A)),1) by A1, A2, A3, A5, A4, A7, A9, MATRIX_4:63

.= (x1 * A) + (x2 * A) by A6, A8, Th55 ; :: thesis: verum

(x1 + x2) * A = (x1 * A) + (x2 * A)

let A be Matrix of REAL; :: thesis: ( len x1 = len x2 & len A = len x1 & len x1 > 0 implies (x1 + x2) * A = (x1 * A) + (x2 * A) )

assume that

A1: len x1 = len x2 and

A2: len A = len x1 and

A3: len x1 > 0 ; :: thesis: (x1 + x2) * A = (x1 * A) + (x2 * A)

A4: width (LineVec2Mx x2) = len x2 by Def10;

A5: width (LineVec2Mx x1) = len x1 by Def10;

then A6: width ((LineVec2Mx x1) * A) = width A by A2, MATRIX_3:def 4

.= width ((LineVec2Mx x2) * A) by A1, A2, A4, MATRIX_3:def 4 ;

A7: len (LineVec2Mx x1) = 1 by Def10;

then A8: 1 <= len ((LineVec2Mx x1) * A) by A2, A5, MATRIX_3:def 4;

A9: len (LineVec2Mx x2) = 1 by Def10;

thus (x1 + x2) * A = Line ((((LineVec2Mx x1) + (LineVec2Mx x2)) * A),1) by A1, Th50

.= Line ((((LineVec2Mx x1) * A) + ((LineVec2Mx x2) * A)),1) by A1, A2, A3, A5, A4, A7, A9, MATRIX_4:63

.= (x1 * A) + (x2 * A) by A6, A8, Th55 ; :: thesis: verum