let m, l, n be Nat; :: thesis:
let S be Matrix of l,m,INT.Ring; :: thesis:
let T be Matrix of m,n,INT.Ring; :: thesis:
let S1 be Matrix of l,m,F_Real; :: thesis:
let T1 be Matrix of m,n,F_Real; :: thesis:
assume AS: ( S = S1 & T = T1 & 0 < l & 0 < m ) ; :: thesis:
P1: ( len S = l & width S = m & Indices S = [:(Seg l),(Seg m):] ) by MATRIX_0:23, AS;
Q1: ( len S1 = l & width S1 = m & Indices S1 = [:(Seg l),(Seg m):] ) by MATRIX_0:23, AS;
P2: ( len T = m & width T = n & Indices T = [:(Seg m),(Seg n):] ) by MATRIX_0:23, AS;
Q2: ( len T1 = m & width T1 = n & Indices T1 = [:(Seg m),(Seg n):] ) by MATRIX_0:23, AS;
P3: ( len (S * T) = len S & width (S * T) = width T ) by P1, P2, MATRIX_3:def 4;
Q3: ( len (S1 * T1) = len S1 & width (S1 * T1) = width T1 ) by Q1, Q2, MATRIX_3:def 4;
reconsider ST = S * T as Matrix of l,n,INT.Ring by P3, AS, P1, P2, MATRIX_0:20;
reconsider S1T1 = S1 * T1 as Matrix of l,n,F_Real by Q3, AS, Q1, Q2, MATRIX_0:20;
for i, j being Nat st [i,j] in Indices ST holds
ST * (i,j) = S1T1 * (i,j)

proof

let i, j be Nat; :: thesis:
assume A1: [i,j] in Indices ST ; :: thesis:
A2: Indices ST = [:(Seg (len ST)),(Seg (width ST)):] by FINSEQ_1:def 3
.= Indices S1T1 by AS, P3, Q3, FINSEQ_1:def 3 ;
i in dom ST by A1, ZFMISC_1:87;
then i in Seg (len ST) by FINSEQ_1:def 3;
then i in dom S by FINSEQ_1:def 3, P3;
then X1: Line (S,i) = Line (S1,i) by ZMATRLIN:2, AS;
j in Seg (width T) by A1, P3, ZFMISC_1:87;
then X2: Col (T,j) = Col (T1,j) by ZMATRLIN:3, AS;
thus ST * (i,j) = (Line (S,i)) "*" (Col (T,j)) by A1, P1, P2, MATRIX_3:def 4
.= (Line (S1,i)) "*" (Col (T1,j)) by X1, X2, ZMATRLIN:37
.= S1T1 * (i,j) by A1, A2, Q1, Q2, MATRIX_3:def 4 ; :: thesis:

end;

hence S * T = S1 * T1 by AS, P3, Q3, ZMATRLIN:4; :: thesis: