let x1, x2 be FinSequence of REAL ; 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; ( 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
; (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
; verum