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 ;
A4: j in Seg () by ;
A5: ( dom C = Seg (len C) & len C = len (k |-> (0. K)) ) by ;
then width C = 1 by A3, A1, Th26;
then A6: j = 1 by ;
Indices (0. (K,k,1)) = Indices C by MATRIX_0:26;
hence (0. (K,k,1)) * (i,j) = 0. K by
.= (k |-> (0. K)) . i by
.= (Col (C,j)) . i by A3, A5, A1, A6, Th26
.= C * (i,j) by ;
:: thesis: verum
end;
hence ColVec2Mx (k |-> (0. K)) = 0. (K,k,1) by MATRIX_0:27; :: thesis: verum