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;

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 )
;

end;

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;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

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;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