let n be Nat; :: thesis: for K being Field
for M being V239(b₁) Matrix of n,K holds M @ = M
let K be Field; :: thesis: for M being V239(K) Matrix of n,K holds M @ = M
let M be V239(K) Matrix of n,K; :: thesis: M @ = M
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (M @) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) = (M @) * (i,j) )
assume A1: [i,j] in Indices M ; :: thesis: M * (i,j) = (M @) * (i,j)
then A2: [j,i] in Indices M by MATRIX_1:28;
then A3: (M @) * (i,j) = M * (j,i) by MATRIX_1:def 6;

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: M * (i,j) = (M @) * (i,j)

hence M * (i,j) = (M @) * (i,j) by A1, MATRIX_1:def 6; :: thesis: verum

end;

suppose A4: i <> j ; :: thesis: M * (i,j) = (M @) * (i,j)

then M * (i,j) = 0. K by A1, MATRIX_1:def 14;
hence M * (i,j) = (M @) * (i,j) by A2, A3, A4, MATRIX_1:def 14; :: thesis: verum

end;

end;

end;

hence M @ = M by MATRIX_1:27; :: thesis: verum