let i be Nat; :: thesis:
let K be Field; :: thesis:
let A, B be Matrix of K; :: thesis:
assume that
A1: i in dom A and
A2: width A = len B ; :: thesis:
A3: width (A * B) = width B by A2, MATRIX_3:def 4;
set LAB = LineVec2Mx (Line ((A * B),i));
A4: ( width (LineVec2Mx (Line ((A * B),i))) = len (Line ((A * B),i)) & len (Line ((A * B),i)) = width (A * B) ) by CARD_1:def 7, MATRIX_0:23;
set L = LineVec2Mx (Line (A,i));
A5: ( width (LineVec2Mx (Line (A,i))) = len (Line (A,i)) & len (Line (A,i)) = width A ) by CARD_1:def 7, MATRIX_0:23;
then A6: width ((LineVec2Mx (Line (A,i))) * B) = width B by A2, MATRIX_3:def 4;
len (LineVec2Mx (Line (A,i))) = 1 by CARD_1:def 7;
then A7: len ((LineVec2Mx (Line (A,i))) * B) = 1 by A2, A5, MATRIX_3:def 4;
len (A * B) = len A by A2, MATRIX_3:def 4;
then A8: dom A = dom (A * B) by FINSEQ_3:29;

A9: now :: thesis:

let j, k be Nat; :: thesis:
assume A10: [j,k] in Indices ((LineVec2Mx (Line (A,i))) * B) ; :: thesis:
A11: k in Seg (width (A * B)) by A3, A6, A10, ZFMISC_1:87;
then A12: [i,k] in Indices (A * B) by A1, A8, ZFMISC_1:87;
Indices ((LineVec2Mx (Line (A,i))) * B) = [:(Seg 1),(Seg (width B)):] by A7, A6, FINSEQ_1:def 3;
then j in Seg 1 by A10, ZFMISC_1:87;
then A13: j = 1 by FINSEQ_1:2, TARSKI:def 1;
hence ((LineVec2Mx (Line (A,i))) * B) * (j,k) = (Line ((LineVec2Mx (Line (A,i))),1)) "*" (Col (B,k)) by A2, A5, A10, MATRIX_3:def 4
.= (Line (A,i)) "*" (Col (B,k)) by MATRIX15:25
.= (A * B) * (i,k) by A2, A12, MATRIX_3:def 4
.= (Line ((A * B),i)) . k by A11, MATRIX_0:def 7
.= (Line ((LineVec2Mx (Line ((A * B),i))),j)) . k by A13, MATRIX15:25
.= (LineVec2Mx (Line ((A * B),i))) * (j,k) by A4, A11, MATRIX_0:def 7 ;
:: thesis:

end;

len (LineVec2Mx (Line ((A * B),i))) = 1 by CARD_1:def 7;
hence (LineVec2Mx (Line (A,i))) * B = LineVec2Mx (Line ((A * B),i)) by A4, A3, A7, A6, A9, MATRIX_0:21; :: thesis: