let k be Nat; :: thesis: for K being Field holds ColVec2Mx (k |-> (0. K)) = 0. K,k,1
let K be Field; :: thesis: ColVec2Mx (k |-> (0. K)) = 0. K,k,1
reconsider C = ColVec2Mx (k |-> (0. K)) as Matrix of k,1,K by FINSEQ_1:def 18;
set Z = 0. K,k,1;

now

A1: len (k |-> (0. K)) = k by FINSEQ_1:def 18;
let i, j be Nat; :: thesis: ( [i,j] in Indices C implies (0. K,k,1) * i,j = C * i,j )
assume A2: [i,j] in Indices C ; :: thesis: (0. K,k,1) * i,j = C * i,j
A3: i in dom C by A2, ZFMISC_1:106;
A4: j in Seg (width C) by A2, ZFMISC_1:106;
A5: ( dom C = Seg (len C) & len C = len (k |-> (0. K)) ) by FINSEQ_1:def 3, MATRIX_1:def 3;
then width C = 1 by A3, A1, Th26;
then A6: j = 1 by A4, FINSEQ_1:4, TARSKI:def 1;
Indices (0. K,k,1) = Indices C by MATRIX_1:27;
hence (0. K,k,1) * i,j = 0. K by A2, MATRIX_3:3
.= (k |-> (0. K)) . i by A3, A5, A1, FINSEQ_2:71
.= (Col C,j) . i by A3, A5, A1, A6, Th26
.= C * i,j by A3, MATRIX_1:def 9 ;
:: thesis: verum

end;

hence ColVec2Mx (k |-> (0. K)) = 0. K,k,1 by MATRIX_1:28; :: thesis: verum