let n be Nat; for K being Field
for M being V254(b1) Matrix of n,K holds M @ = M
let K be Field; for M being V254(K) Matrix of n,K holds M @ = M
let M be V254(K) Matrix of n,K; 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;
( [i,j] in Indices M implies M * (i,j) = (M @) * (i,j) )
assume A1:
[i,j] in Indices M
;
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;
hence
M @ = M
by MATRIX_0:27; verum