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

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