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 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 implies x * (A + B) = (x * A) + (x * B) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: len A = len x ; :: thesis: x * (A + B) = (x * A) + (x * B)
A4: width (LineVec2Mx x) = len x by Def10;
then A5: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A2, MATRIX_3:def 4
.= 1 by Def10 ;
A6: width ((LineVec2Mx x) * A) = width A by A2, A4, MATRIX_3:def 4
.= width ((LineVec2Mx x) * B) by A1, A2, A4, MATRIX_3:def 4 ;
thus x * (A + B) = Line ((((LineVec2Mx x) * A) + ((LineVec2Mx x) * B)),1) by A1, A2, A4, MATRIX_4:62
.= (x * A) + (x * B) by A6, A5, Th55 ; :: thesis: verum