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