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

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

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

assume that

A1: len x1 = len x2 and

A2: width A = len x1 and

A3: len x1 > 0 and

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

A5: len (ColVec2Mx x2) = len x2 by A1, A3, Def9;

A6: len (ColVec2Mx x1) = len x1 by A3, Def9;

then A7: len (A * (ColVec2Mx x1)) = len A by A2, MATRIX_3:def 4

.= len (A * (ColVec2Mx x2)) by A1, A2, A5, MATRIX_3:def 4 ;

A8: width (ColVec2Mx x1) = 1 by A3, Def9;

then A9: 1 <= width (A * (ColVec2Mx x1)) by A2, A6, MATRIX_3:def 4;

A10: width (ColVec2Mx x2) = 1 by A1, A3, Def9;

thus A * (x1 + x2) = Col ((A * ((ColVec2Mx x1) + (ColVec2Mx x2))),1) by A1, A3, Th46

.= Col (((A * (ColVec2Mx x1)) + (A * (ColVec2Mx x2))),1) by A1, A2, A3, A4, A6, A5, A8, A10, MATRIX_4:62

.= (A * x1) + (A * x2) by A7, A9, Th54 ; :: thesis: verum

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

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

assume that

A1: len x1 = len x2 and

A2: width A = len x1 and

A3: len x1 > 0 and

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

A5: len (ColVec2Mx x2) = len x2 by A1, A3, Def9;

A6: len (ColVec2Mx x1) = len x1 by A3, Def9;

then A7: len (A * (ColVec2Mx x1)) = len A by A2, MATRIX_3:def 4

.= len (A * (ColVec2Mx x2)) by A1, A2, A5, MATRIX_3:def 4 ;

A8: width (ColVec2Mx x1) = 1 by A3, Def9;

then A9: 1 <= width (A * (ColVec2Mx x1)) by A2, A6, MATRIX_3:def 4;

A10: width (ColVec2Mx x2) = 1 by A1, A3, Def9;

thus A * (x1 + x2) = Col ((A * ((ColVec2Mx x1) + (ColVec2Mx x2))),1) by A1, A3, Th46

.= Col (((A * (ColVec2Mx x1)) + (A * (ColVec2Mx x2))),1) by A1, A2, A3, A4, A6, A5, A8, A10, MATRIX_4:62

.= (A * x1) + (A * x2) by A7, A9, Th54 ; :: thesis: verum