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 A3: ex p being FinSequence of D1 st

( p = A . i & A * (i,j) = p . j ) by MATRIX_0:def 5;

ex q being FinSequence of D2 st

( q = B . i & B * (i,j) = q . j ) by A1, A2, MATRIX_0:def 5;

hence A * (i,j) = B * (i,j) by A1, A3; :: thesis: verum

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 A3: ex p being FinSequence of D1 st

( p = A . i & A * (i,j) = p . j ) by MATRIX_0:def 5;

ex q being FinSequence of D2 st

( q = B . i & B * (i,j) = q . j ) by A1, A2, MATRIX_0:def 5;

hence A * (i,j) = B * (i,j) by A1, A3; :: thesis: verum