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

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)

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