let n, m, k be Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * i,j = ((Line B,i) * A) . j
let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices (B * A) implies (B * A) * i,j = ((Line B,i) * A) . j )
assume A2: [i,j] in Indices (B * A) ; :: thesis: (B * A) * i,j = ((Line B,i) * A) . j
then A3: ( i in dom (B * A) & j in Seg (width (B * A)) ) by ZFMISC_1:106;
A4: len A = m by MATRIX_1:def 3;
A5: width B = m by A1, MATRIX_1:24;
A6: width B = len A by A1, A4, MATRIX_1:24;
A7: (B * A) * i,j = (Line B,i) "*" (Col A,j) by A2, A6, MATRPROB:39;
A8: len A = len (Line B,i) by A4, A5, MATRIX_1:def 8;
width A = width (B * A) by A4, A5, MATRPROB:39;
then j in Seg (len ((Line B,i) * A)) by A3, A8, MATRIXR1:62;
hence (B * A) * i,j = ((Line B,i) * A) . j by A7, A8, MATRPROB:40; :: thesis: verum