let n be Nat; :: thesis: for K being Field

for M being V254(b_{1}) 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)

for M being V254(b

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

hence
M @ = M
by MATRIX_0:27; :: thesis: verum
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;

end;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;