let i be Nat; :: thesis: for K being Field
for A, B being Matrix of K st i in dom A & width A = len B holds
(LineVec2Mx (Line A,i)) * B = LineVec2Mx (Line (A * B),i)
let K be Field; :: thesis: for A, B being Matrix of K st i in dom A & width A = len B holds
(LineVec2Mx (Line A,i)) * B = LineVec2Mx (Line (A * B),i)
let A, B be Matrix of K; :: thesis: ( i in dom A & width A = len B implies (LineVec2Mx (Line A,i)) * B = LineVec2Mx (Line (A * B),i) )
assume that
A1: i in dom A and
A2: width A = len B ; :: thesis: (LineVec2Mx (Line A,i)) * B = LineVec2Mx (Line (A * B),i)
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 FINSEQ_1:def 18, MATRIX_1:24;
set L = LineVec2Mx (Line A,i);
A5: ( width (LineVec2Mx (Line A,i)) = len (Line A,i) & len (Line A,i) = width A ) by FINSEQ_1:def 18, MATRIX_1:24;
then A6: width ((LineVec2Mx (Line A,i)) * B) = width B by A2, MATRIX_3:def 4;
len (LineVec2Mx (Line A,i)) = 1 by FINSEQ_1:def 18;
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:31;

A9: now

let j, k be Nat; :: thesis: ( [j,k] in Indices ((LineVec2Mx (Line A,i)) * B) implies ((LineVec2Mx (Line A,i)) * B) * j,k = (LineVec2Mx (Line (A * B),i)) * j,k )
assume A10: [j,k] in Indices ((LineVec2Mx (Line A,i)) * B) ; :: thesis: ((LineVec2Mx (Line A,i)) * B) * j,k = (LineVec2Mx (Line (A * B),i)) * j,k
A11: k in Seg (width (A * B)) by A3, A6, A10, ZFMISC_1:106;
then A12: [i,k] in Indices (A * B) by A1, A8, ZFMISC_1:106;
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:106;
then A13: j = 1 by FINSEQ_1:4, 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_1:def 8
.= (Line (LineVec2Mx (Line (A * B),i)),j) . k by A13, MATRIX15:25
.= (LineVec2Mx (Line (A * B),i)) * j,k by A4, A11, MATRIX_1:def 8 ;
:: thesis: verum

end;

len (LineVec2Mx (Line (A * B),i)) = 1 by FINSEQ_1:def 18;
hence (LineVec2Mx (Line A,i)) * B = LineVec2Mx (Line (A * B),i) by A4, A3, A7, A6, A9, MATRIX_1:21; :: thesis: verum