let k be Nat; :: thesis: for K being Field holds LineVec2Mx (k |-> (0. K)) = 0. K,1,k
let K be Field; :: thesis: LineVec2Mx (k |-> (0. K)) = 0. K,1,k
reconsider L = LineVec2Mx (k |-> (0. K)) as Matrix of 1,k,K by FINSEQ_1:def 18;
set Z = 0. K,1,k;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices L implies (0. K,1,k) * i,j = L * i,j )
assume A1: [i,j] in Indices L ; :: thesis: (0. K,1,k) * i,j = L * i,j
A2: ( j in Seg (width L) & i in dom L & dom L = Seg (len L) & len L = 1 ) by A1, FINSEQ_1:def 3, MATRIX_1:def 3, ZFMISC_1:106;
then A3: i = 1 by FINSEQ_1:4, TARSKI:def 1;
A4: width L = k by MATRIX_1:24;
Indices (0. K,1,k) = Indices L by MATRIX_1:27;
hence (0. K,1,k) * i,j = 0. K by A1, MATRIX_3:3
.= (k |-> (0. K)) . j by A2, A4, FINSEQ_2:71
.= (Line L,i) . j by A3, Th25
.= L * i,j by A2, MATRIX_1:def 8 ;
:: thesis: verum

end;

hence LineVec2Mx (k |-> (0. K)) = 0. K,1,k by MATRIX_1:28; :: thesis: verum