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

now

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

end;

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