let D, E be non empty set ; :: thesis: for M being Matrix of D
for L being Matrix of E st M = L holds
M @ = L @
let M be Matrix of D; :: thesis: for L being Matrix of E st M = L holds
M @ = L @
let L be Matrix of E; :: thesis: ( M = L implies M @ = L @ )
assume AS: M = L ; :: thesis: M @ = L @
for i, j being Nat st [i,j] in Indices (M @) holds
(M @) * (i,j) in E

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) in E )
assume [i,j] in Indices (M @) ; :: thesis: (M @) * (i,j) in E
then A2: [j,i] in Indices M by MATRIX_0:def 6;
then (M @) * (i,j) = M * (j,i) by MATRIX_0:def 6
.= L * (j,i) by AS, A2, EQ2 ;
hence (M @) * (i,j) in E ; :: thesis: verum

end;

then reconsider M1 = M @ as Matrix of E by REALTOINT;
P1: len M1 = width L by AS, MATRIX_0:def 6;
P2: for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices L ) by AS, MATRIX_0:def 6;
for i, j being Nat st [j,i] in Indices L holds
M1 * (i,j) = L * (j,i)

proof

let i, j be Nat; :: thesis: ( [j,i] in Indices L implies M1 * (i,j) = L * (j,i) )
assume A2: [j,i] in Indices L ; :: thesis: M1 * (i,j) = L * (j,i)
then [i,j] in Indices (M @) by AS, MATRIX_0:def 6;
then M1 * (i,j) = (M @) * (i,j) by EQ2
.= M * (j,i) by AS, A2, MATRIX_0:def 6 ;
hence M1 * (i,j) = L * (j,i) by AS, A2, EQ2; :: thesis: verum

end;

hence M @ = L @ by P1, P2, MATRIX_0:def 6; :: thesis: verum