let x be FinSequence of REAL ; for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x & len x > 0 holds
x * (A + B) = (x * A) + (x * B)
let A, B be Matrix of REAL; ( len A = len B & width A = width B & len A = len x & len x > 0 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
and
A3:
len x > 0
; 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
;
len (LineVec2Mx x) = 1
by Def10;
hence x * (A + B) =
Line ((((LineVec2Mx x) * A) + ((LineVec2Mx x) * B)),1)
by A1, A2, A3, A4, MATRIX_4:62
.=
(x * A) + (x * B)
by A6, A5, Th55
;
verum