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