let D be non empty set ; :: thesis: for M being Matrix of D st len M > 0 & width M > 0 holds
(M @ ) @ = M
let M be Matrix of D; :: thesis: ( len M > 0 & width M > 0 implies (M @ ) @ = M )
assume A1: ( len M > 0 & width M > 0 ) ; :: thesis: (M @ ) @ = M
set N = M @ ;
A2: ( len (M @ ) = width M & ( for i, j being Nat holds
( [i,j] in Indices (M @ ) iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
(M @ ) * i,j = M * j,i ) ) by MATRIX_1:def 7;
A3: width (M @ ) = len M by A1, Th12;
A4: width (M @ ) > 0 by A1, Th12;
A5: ( len ((M @ ) @ ) = width (M @ ) & ( for i, j being Nat holds
( [i,j] in Indices ((M @ ) @ ) iff [j,i] in Indices (M @ ) ) ) & ( for i, j being Nat st [j,i] in Indices (M @ ) holds
((M @ ) @ ) * i,j = (M @ ) * j,i ) ) by MATRIX_1:def 7;
A6: width ((M @ ) @ ) = width M by A2, A4, Th12;
( dom M = Seg (len M) & dom ((M @ ) @ ) = Seg (len ((M @ ) @ )) ) by FINSEQ_1:def 3;
then A7: Indices ((M @ ) @ ) = Indices M by A1, A2, A3, A5, Th12;
for i, j being Nat st [i,j] in Indices ((M @ ) @ ) holds
((M @ ) @ ) * i,j = M * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((M @ ) @ ) implies ((M @ ) @ ) * i,j = M * i,j )
assume A8: [i,j] in Indices ((M @ ) @ ) ; :: thesis: ((M @ ) @ ) * i,j = M * i,j
then [j,i] in Indices (M @ ) by MATRIX_1:def 7;
then ((M @ ) @ ) * i,j = (M @ ) * j,i by MATRIX_1:def 7;
hence ((M @ ) @ ) * i,j = M * i,j by A7, A8, MATRIX_1:def 7; :: thesis: verum

end;

hence (M @ ) @ = M by A3, A5, A6, MATRIX_1:21; :: thesis: verum