let k be Nat; for K being Field holds ColVec2Mx (k |-> (0. K)) = 0. (K,k,1)
let K be Field; 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 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;
( [i,j] in Indices C implies (0. (K,k,1)) * (i,j) = C * (i,j) )assume A2:
[i,j] in Indices C
;
(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
;
verum end;
hence
ColVec2Mx (k |-> (0. K)) = 0. (K,k,1)
by MATRIX_0:27; verum