let x be FinSequence of REAL ; :: thesis: for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x & width A > 0 & len x > 0 holds
x * (A + B) = (x * A) + (x * B)
let A, B be Matrix of REAL ; :: thesis: ( len A = len B & width A = width B & len A = len x & width A > 0 & len x > 0 implies x * (A + B) = (x * A) + (x * B) )
assume A1: ( len A = len B & width A = width B & len A = len x & width A > 0 & len x > 0 ) ; :: thesis: x * (A + B) = (x * A) + (x * B)
A2: width (LineVec2Mx x) = len x by Def10;
A3: len (LineVec2Mx x) = 1 by Def10;
A4: width ((LineVec2Mx x) * A) = width A by A1, A2, MATRIX_3:def 4
.= width ((LineVec2Mx x) * B) by A1, A2, MATRIX_3:def 4 ;
A5: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A2, MATRIX_3:def 4
.= len ((LineVec2Mx x) * B) by A1, A2, MATRIX_3:def 4 ;
A6: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A2, MATRIX_3:def 4
.= 1 by Def10 ;
thus x * (A + B) = Line (((LineVec2Mx x) * A) + ((LineVec2Mx x) * B)),1 by A1, A2, A3, MATRIX_4:62
.= (x * A) + (x * B) by A4, A5, A6, Th55 ; :: thesis: verum