let M be Matrix of COMPLEX ; :: thesis: (M *' ) *' = M
A1: len ((M *' ) *' ) = len (M *' ) by Def1;
A2: len (M *' ) = len M by Def1;
A3: width ((M *' ) *' ) = width (M *' ) by Def1;
A4: width (M *' ) = width M by Def1;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices ((M *' ) *' ) implies ((M *' ) *' ) * i,j = M * i,j )
assume [i,j] in Indices ((M *' ) *' ) ; :: thesis: ((M *' ) *' ) * i,j = M * i,j
then A5: ( 1 <= i & i <= len (M *' ) & 1 <= j & j <= width (M *' ) ) by A1, A3, Th1;
then A6: [i,j] in Indices (M *' ) by Th1;
[i,j] in Indices M by A2, A4, A5, Th1;
then (M *' ) * i,j = (M * i,j) *' by Def1;
hence ((M *' ) *' ) * i,j = ((M * i,j) *' ) *' by A6, Def1
.= M * i,j ;
:: thesis: verum

end;

hence (M *' ) *' = M by A1, A2, A3, A4, MATRIX_1:21; :: thesis: verum