let D be non empty set ; for n being Nat
for A being Matrix of n,D holds (A @) @ = A
let n be Nat; for A being Matrix of n,D holds (A @) @ = A
let A be Matrix of n,D; (A @) @ = A
reconsider N = A @ as Matrix of n,D ;
A1:
( len A = n & width A = n )
by MATRIX_0:24;
A2: Indices (N @) =
[:(Seg n),(Seg n):]
by MATRIX_0:24
.=
Indices A
by MATRIX_0:24
;
A3:
for i, j being Nat st [i,j] in Indices (N @) holds
(N @) * (i,j) = A * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices (N @) implies (N @) * (i,j) = A * (i,j) )
assume A4:
[i,j] in Indices (N @)
;
(N @) * (i,j) = A * (i,j)
then
[j,i] in Indices N
by MATRIX_0:def 6;
then
(N @) * (
i,
j)
= N * (
j,
i)
by MATRIX_0:def 6;
hence
(N @) * (
i,
j)
= A * (
i,
j)
by A2, A4, MATRIX_0:def 6;
verum
end;
( len (N @) = n & width (N @) = n )
by MATRIX_0:24;
hence
(A @) @ = A
by A1, A3, MATRIX_0:21; verum