let n be Nat; :: thesis: for K being Field
for M being V254(b1) Matrix of n,K holds M @ = M
let K be Field; :: thesis: for M being V254(K) Matrix of n,K holds M @ = M
let M be V254(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_0:28;
then A3: (M @) * (i,j) = M * (j,i) by MATRIX_0: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_0: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 6;
hence M * (i,j) = (M @) * (i,j) by A2, A3, A4, MATRIX_1:def 6; :: thesis: verum
end;
end;
end;
hence M @ = M by MATRIX_0:27; :: thesis: verum