let k be Nat; for K being Field holds LineVec2Mx (k |-> (0. K)) = 0. (K,1,k)
let K be Field; LineVec2Mx (k |-> (0. K)) = 0. (K,1,k)
card (k |-> (0. K)) = k
by CARD_1:def 7;
then reconsider L = LineVec2Mx (k |-> (0. K)) as Matrix of 1,k,K ;
set Z = 0. (K,1,k);
now for i, j being Nat st [i,j] in Indices L holds
(0. (K,1,k)) * (i,j) = L * (i,j)A1:
width L = k
by MATRIX_0:23;
A2:
(
dom L = Seg (len L) &
len L = 1 )
by FINSEQ_1:def 3, MATRIX_0:def 2;
let i,
j be
Nat;
( [i,j] in Indices L implies (0. (K,1,k)) * (i,j) = L * (i,j) )assume A3:
[i,j] in Indices L
;
(0. (K,1,k)) * (i,j) = L * (i,j)A4:
j in Seg (width L)
by A3, ZFMISC_1:87;
i in dom L
by A3, ZFMISC_1:87;
then A5:
i = 1
by A2, FINSEQ_1:2, TARSKI:def 1;
Indices (0. (K,1,k)) = Indices L
by MATRIX_0:26;
hence (0. (K,1,k)) * (
i,
j) =
0. K
by A3, MATRIX_3:1
.=
(k |-> (0. K)) . j
by A4, A1, FINSEQ_2:57
.=
(Line (L,i)) . j
by A5, Th25
.=
L * (
i,
j)
by A4, MATRIX_0:def 7
;
verum end;
hence
LineVec2Mx (k |-> (0. K)) = 0. (K,1,k)
by MATRIX_0:27; verum