let k, n, m be Nat; :: thesis: for B being Matrix of n,m,REAL
for A being Matrix of m,k,REAL st n > 0 holds
for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
let B be Matrix of n,m,REAL; :: thesis: for A being Matrix of m,k,REAL st n > 0 holds
for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
let A be Matrix of m,k,REAL; :: thesis: ( n > 0 implies for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j )
assume A1: n > 0 ; :: thesis: for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
then A2: width B = m by MATRIX_0:23;
let i, j be Nat; :: thesis: ( [i,j] in Indices (B * A) implies (B * A) * (i,j) = ((Line (B,i)) * A) . j )
A3: len A = m by MATRIX_0:def 2;
then A4: len A = len (Line (B,i)) by A2, MATRIX_0:def 7;
assume A5: [i,j] in Indices (B * A) ; :: thesis: (B * A) * (i,j) = ((Line (B,i)) * A) . j
then A6: j in Seg (width (B * A)) by ZFMISC_1:87;
width B = len A by A1, A3, MATRIX_0:23;
then A7: (B * A) * (i,j) = (Line (B,i)) "*" (Col (A,j)) by A5, MATRPROB:39;
width A = width (B * A) by A3, A2, MATRPROB:39;
then j in Seg (len ((Line (B,i)) * A)) by A6, A4, MATRIXR1:62;
hence (B * A) * (i,j) = ((Line (B,i)) * A) . j by A7, A4, MATRPROB:40; :: thesis: verum