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 )
A2: width A = n by MATRIX_1:25;
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:106;
then A4: i in Seg (len (A * B)) by FINSEQ_1:def 3;
A5: len B = n by MATRIX_1:def 3;
then A6: width A = len (Col B,j) by A2, MATRIX_1:def 9;
width A = len B by A5, MATRIX_1:25;
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_1:25;
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