let D1, D2 be set ; :: thesis: for A being Matrix of D1
for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * i,j = B * i,j
let A be Matrix of D1; :: thesis: for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * i,j = B * i,j
let B be Matrix of D2; :: thesis: ( A = B implies for i, j being Nat st [i,j] in Indices A holds
A * i,j = B * i,j )
assume A1: A = B ; :: thesis: for i, j being Nat st [i,j] in Indices A holds
A * i,j = B * i,j
let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * i,j = B * i,j )
assume A2: [i,j] in Indices A ; :: thesis: A * i,j = B * i,j
then consider p being FinSequence of D1 such that
A3: ( p = A . i & A * i,j = p . j ) by MATRIX_1:def 6;
ex q being FinSequence of D2 st
( q = B . i & B * i,j = q . j ) by A1, A2, MATRIX_1:def 6;
hence A * i,j = B * i,j by A1, A3; :: thesis: verum