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)

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

let K be Field; :: thesis: 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 :: thesis: for i, j being Nat st [i,j] in Indices L holds

(0. (K,1,k)) * (i,j) = L * (i,j)

hence
LineVec2Mx (k |-> (0. K)) = 0. (K,1,k)
by MATRIX_0:27; :: thesis: verum(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; :: thesis: ( [i,j] in Indices L implies (0. (K,1,k)) * (i,j) = L * (i,j) )

assume A3: [i,j] in Indices L ; :: thesis: (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 ;

:: thesis: verum

end;A2: ( dom L = Seg (len L) & len L = 1 ) by FINSEQ_1:def 3, MATRIX_0:def 2;

let i, j be Nat; :: thesis: ( [i,j] in Indices L implies (0. (K,1,k)) * (i,j) = L * (i,j) )

assume A3: [i,j] in Indices L ; :: thesis: (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 ;

:: thesis: verum