let n be Element of NAT ; :: thesis: for A, B being Matrix of n, REAL st n > 0 holds
for i, j being Element of 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 Element of 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 Element of NAT st [i,j] in Indices (A * B) holds
(A * B) * i,j = (A * (Col B,j)) . i
let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices (A * B) implies (A * B) * i,j = (A * (Col B,j)) . i )
assume A2: [i,j] in Indices (A * B) ; :: thesis: (A * B) * i,j = (A * (Col B,j)) . i
then ( i in dom (A * B) & j in Seg (width (A * B)) ) by ZFMISC_1:106;
then A3: i in Seg (len (A * B)) by FINSEQ_1:def 3;
A4: ( len (A * B) = n & width (A * B) = n ) by MATRIX_1:25;
A5: len B = n by MATRIX_1:def 3;
A6: ( len A = n & width A = n ) by MATRIX_1:25;
A7: width A = len B by A5, MATRIX_1:25;
A8: (A * B) * i,j = (Line A,i) "*" (Col B,j) by A2, A7, MATRPROB:39;
A9: width A = len (Col B,j) by A5, A6, MATRIX_1:def 9;
then i in Seg (len (A * (Col B,j))) by A1, A3, A4, A6, MATRIXR1:61;
hence (A * B) * i,j = (A * (Col B,j)) . i by A1, A6, A8, A9, MATRPROB:41; :: thesis: verum