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 that
A1: len M > 0 and
A2: width M > 0 ; :: thesis: (M @ ) @ = M
set N = M @ ;
A3: width (M @ ) = len M by A2, Th12;
A4: len ((M @ ) @ ) = width (M @ ) by MATRIX_1:def 7;
A5: len (M @ ) = width M by MATRIX_1:def 7;
( dom M = Seg (len M) & dom ((M @ ) @ ) = Seg (len ((M @ ) @ )) ) by FINSEQ_1:def 3;
then A6: Indices ((M @ ) @ ) = Indices M by A1, A5, A3, A4, Th12;
A7: 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 A6, A8, MATRIX_1:def 7; :: thesis: verum

end;

width (M @ ) > 0 by A1, A2, Th12;
then width ((M @ ) @ ) = width M by A5, Th12;
hence (M @ ) @ = M by A3, A4, A7, MATRIX_1:21; :: thesis: verum