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)
card (k |-> (0. K)) = k by CARD_1:def 7;
then reconsider C = ColVec2Mx (k |-> (0. K)) as Matrix of k,1,K ;
set Z = 0. (K,k,1);

now :: thesis: for i, j being Nat st [i,j] in Indices C holds
(0. (K,k,1)) * (i,j) = C * (i,j)

A1: len (k |-> (0. K)) = k by CARD_1:def 7;
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:87;
A4: j in Seg (width C) by A2, ZFMISC_1:87;
A5: ( dom C = Seg (len C) & len C = len (k |-> (0. K)) ) by FINSEQ_1:def 3, MATRIX_0:def 2;
then width C = 1 by A3, A1, Th26;
then A6: j = 1 by A4, FINSEQ_1:2, TARSKI:def 1;
Indices (0. (K,k,1)) = Indices C by MATRIX_0:26;
hence (0. (K,k,1)) * (i,j) = 0. K by A2, MATRIX_3:1
.= (k |-> (0. K)) . i by A3, A5, A1, FINSEQ_2:57
.= (Col (C,j)) . i by A3, A5, A1, A6, Th26
.= C * (i,j) by A3, MATRIX_0:def 8 ;
:: thesis: verum

end;

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