let R be Ring; :: thesis: for n being Nat
for S being Subring of R
for a, b being Matrix of n,S
for A, B being Matrix of n,R st a = A & b = B holds
a * b = A * B
let n be Nat; :: thesis: for S being Subring of R
for a, b being Matrix of n,S
for A, B being Matrix of n,R st a = A & b = B holds
a * b = A * B
let S be Subring of R; :: thesis: for a, b being Matrix of n,S
for A, B being Matrix of n,R st a = A & b = B holds
a * b = A * B
let a, b be Matrix of n,S; :: thesis: for A, B being Matrix of n,R st a = A & b = B holds
a * b = A * B
let A, B be Matrix of n,R; :: thesis: ( a = A & b = B implies a * b = A * B )
assume A1: ( a = A & b = B ) ; :: thesis: a * b = A * B
set LHS = a * b;
set RHS = A * B;
A2: width a = n by MATRIX_0:24
.= len b by MATRIX_0:25 ;
A3: width A = n by MATRIX_0:24
.= len B by MATRIX_0:25 ;
for i, j being Nat st [i,j] in Indices (a * b) holds
(a * b) * (i,j) = (A * B) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * b) implies (a * b) * (i,j) = (A * B) * (i,j) )
assume A4: [i,j] in Indices (a * b) ; :: thesis: (a * b) * (i,j) = (A * B) * (i,j)
A5: Indices (a * b) = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices (A * B) by MATRIX_0:24 ;
A6: ( i in dom a & j in Seg (width b) )

proof

[i,j] in [:(dom (a * b)),(Seg (width (a * b))):] by A4, MATRIX_0:def 4;
then A7: ( i in dom (a * b) & j in Seg (width (a * b)) ) by ZFMISC_1:87;
len (a * b) = len a by A2, MATRIX_3:def 4;
then Seg (len (a * b)) = dom a by FINSEQ_1:def 3;
hence i in dom a by A7, FINSEQ_1:def 3; :: thesis: j in Seg (width b)
thus j in Seg (width b) by A2, A7, MATRIX_3:def 4; :: thesis: verum

end;

then A8: Line (a,i) = Line (A,i) by A1, Th88;
Col (b,j) = Col (B,j) by A1, A6, Th89;
then A9: Sum (mlt ((Line (a,i)),(Col (b,j)))) = Sum (mlt ((Line (A,i)),(Col (B,j)))) by A8, Th90, Th91;
thus (a * b) * (i,j) = (Line (a,i)) "*" (Col (b,j)) by A2, A4, MATRIX_3:def 4
.= Sum (mlt ((Line (a,i)),(Col (b,j)))) by FVSUM_1:def 9
.= (Line (A,i)) "*" (Col (B,j)) by A9, FVSUM_1:def 9
.= (A * B) * (i,j) by A3, A4, A5, MATRIX_3:def 4 ; :: thesis: verum

end;

hence a * b = A * B by Th83; :: thesis: verum