let D, E be non empty set ; :: thesis: for M being Matrix of D
for L being Matrix of E
for i, j being Nat st M = L & [i,j] in Indices M holds
M * (i,j) = L * (i,j)
let M be Matrix of D; :: thesis: for L being Matrix of E
for i, j being Nat st M = L & [i,j] in Indices M holds
M * (i,j) = L * (i,j)
let L be Matrix of E; :: thesis: for i, j being Nat st M = L & [i,j] in Indices M holds
M * (i,j) = L * (i,j)
let i, j be Nat; :: thesis: ( M = L & [i,j] in Indices M implies M * (i,j) = L * (i,j) )
assume AS1: ( M = L & [i,j] in Indices M ) ; :: thesis: M * (i,j) = L * (i,j)
then consider p being FinSequence of D such that
A1: ( p = M . i & M * (i,j) = p . j ) by MATRIX_0:def 5;
consider q being FinSequence of E such that
A2: ( q = L . i & L * (i,j) = q . j ) by MATRIX_0:def 5, AS1;
thus M * (i,j) = L * (i,j) by AS1, A1, A2; :: thesis: verum