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