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