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 (a * (LineVec2Mx f)) = len (LineVec2Mx f) by MATRIX_3:def 5;
A2: len (LineVec2Mx f) = 1 by MATRIX_0:def 2;
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 A2, A1, Th25; :: thesis: verum