let D be non empty set ; :: thesis: for n being Nat
for A being Matrix of n,D holds (A @) @ = A
let n be Nat; :: thesis: for A being Matrix of n,D holds (A @) @ = A
let A be Matrix of n,D; :: thesis: (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; :: thesis: ( [i,j] in Indices (N @) implies (N @) * (i,j) = A * (i,j) )
assume A4: [i,j] in Indices (N @) ; :: thesis: (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; :: thesis: verum

end;

( len (N @) = n & width (N @) = n ) by MATRIX_0:24;
hence (A @) @ = A by A1, A3, MATRIX_0:21; :: thesis: verum