let K be Field; :: thesis: for a being Element of K
for f being FinSequence of K holds a * (ColVec2Mx f) = ColVec2Mx (a * f)
let a be Element of K; :: thesis: for f being FinSequence of K holds a * (ColVec2Mx f) = ColVec2Mx (a * f)
let f be FinSequence of K; :: thesis: a * (ColVec2Mx f) = ColVec2Mx (a * f)
A1: len f = len (a * f) by MATRIXR1:16;

per cases ( len f = 0 or len f > 0 ) ;

suppose len f = 0 ; :: thesis: a * (ColVec2Mx f) = ColVec2Mx (a * f)

then ( len (ColVec2Mx f) = 0 & len (ColVec2Mx (a * f)) = 0 & len (ColVec2Mx f) = len (a * (ColVec2Mx f)) ) by A1, MATRIX_1:def 3, MATRIX_3:def 5;
then ( a * (ColVec2Mx f) = {} & ColVec2Mx (a * f) = {} ) ;
hence a * (ColVec2Mx f) = ColVec2Mx (a * f) ; :: thesis: verum

end;

suppose A2: len f > 0 ; :: thesis: a * (ColVec2Mx f) = ColVec2Mx (a * f)

then A3: ( width (ColVec2Mx f) = 1 & width (a * (ColVec2Mx f)) = width (ColVec2Mx f) & width (ColVec2Mx (a * f)) = 1 ) by A1, MATRIX_1:24, MATRIX_3:def 5;
then Col (a * (ColVec2Mx f)),1 = a * (Col (ColVec2Mx f),1) by MATRIXR1:19
.= a * f by Th26, A2 ;
hence a * (ColVec2Mx f) = ColVec2Mx (a * f) by A1, A2, A3, Th26; :: thesis: verum

end;

end;