let D be non empty set ; :: thesis: for n being Element of NAT
for A being Matrix of n,D holds (A @ ) @ = A
let n be Element of 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_1:25;
A2: Indices (N @ ) = [:(Seg n),(Seg n):] by MATRIX_1:25
.= Indices A by MATRIX_1:25 ;
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_1:def 7;
then (N @ ) * i,j = N * j,i by MATRIX_1:def 7;
hence (N @ ) * i,j = A * i,j by A2, A4, MATRIX_1:def 7; :: thesis: verum

end;

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