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 A2: len f = 0 ; :: thesis: a * (ColVec2Mx f) = ColVec2Mx (a * f)

len (ColVec2Mx f) = len (a * (ColVec2Mx f)) by MATRIX_3:def 5;
then A3: a * (ColVec2Mx f) = {} by A2, MATRIX_0:def 2;
len (ColVec2Mx (a * f)) = 0 by A1, A2, MATRIX_0:def 2;
hence a * (ColVec2Mx f) = ColVec2Mx (a * f) by A3; :: thesis: verum

end;

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

A5: width (a * (ColVec2Mx f)) = width (ColVec2Mx f) by MATRIX_3:def 5;
A6: width (ColVec2Mx f) = 1 by A4, MATRIX_0:23;
then Col ((a * (ColVec2Mx f)),1) = a * (Col ((ColVec2Mx f),1)) by MATRIXR1:19
.= a * f by A4, Th26 ;
hence a * (ColVec2Mx f) = ColVec2Mx (a * f) by A1, A4, A6, A5, Th26; :: thesis: verum

end;

end;