let K be Field; :: thesis: for a being Element of
for f being FinSequence of holds a * (ColVec2Mx f) = ColVec2Mx (a * f)
let a be Element of ; :: thesis: for f being FinSequence of holds a * (ColVec2Mx f) = ColVec2Mx (a * f)
let f be FinSequence of ; :: 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_1:def 3;
len (ColVec2Mx (a * f)) = 0 by A1, A2, MATRIX_1:def 3;
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_1:24;
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;