let K be Field; :: thesis: for a being Element of K
for f being FinSequence of K holds a * (LineVec2Mx f) = LineVec2Mx (a * f)
let a be Element of K; :: thesis: for f being FinSequence of K holds a * (LineVec2Mx f) = LineVec2Mx (a * f)
let f be FinSequence of K; :: thesis: a * (LineVec2Mx f) = LineVec2Mx (a * f)
A1: ( len (LineVec2Mx f) = 1 & len (a * (LineVec2Mx f)) = len (LineVec2Mx f) ) by MATRIX_1:def 3, MATRIX_3:def 5;
then Line (a * (LineVec2Mx f)),1 = a * (Line (LineVec2Mx f),1) by MATRIXR1:20
.= a * f by Th25 ;
hence a * (LineVec2Mx f) = LineVec2Mx (a * f) by A1, Th25; :: thesis: verum