let M be Matrix of COMPLEX ; :: thesis: ( width M > 0 implies (M @ ) *' = (M *' ) @ )
assume A1: width M > 0 ; :: thesis: (M @ ) *' = (M *' ) @
A2: len ((M @ ) *' ) = len (M @ ) by Def1;
A3: width ((M @ ) *' ) = width (M @ ) by Def1;
A4: len ((M @ ) *' ) = len (M @ ) by Def1
.= width M by MATRIX_1:def 7 ;
A5: len ((M *' ) @ ) = width (M *' ) by MATRIX_1:def 7
.= width M by Def1 ;
A6: width ((M @ ) *' ) = width (M @ ) by Def1
.= len M by A1, MATRIX_2:12 ;
width (M *' ) = width M by Def1;
then A7: width ((M *' ) @ ) = len (M *' ) by A1, MATRIX_2:12
.= len M by Def1 ;
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 A9: ( 1 <= i & i <= len (M @ ) & 1 <= j & j <= width (M @ ) ) by A2, A3, Th1;
( 1 <= i & i <= len ((M @ ) *' ) & 1 <= j & j <= width ((M @ ) *' ) ) by A8, Th1;
then A10: ( 1 <= j & j <= len (M *' ) & 1 <= i & i <= width (M *' ) ) by A4, A6, Def1;
A11: [i,j] in Indices (M @ ) by A9, Th1;
then A12: [j,i] in Indices M by MATRIX_1:def 7;
A13: [j,i] in Indices (M *' ) by A10, Th1;
((M @ ) *' ) * i,j = ((M @ ) * i,j) *' by A11, Def1
.= (M * j,i) *' by A12, MATRIX_1:def 7
.= (M *' ) * j,i by A12, Def1
.= ((M *' ) @ ) * i,j by A13, MATRIX_1:def 7 ;
hence ((M @ ) *' ) * i,j = ((M *' ) @ ) * i,j ; :: thesis: verum

end;

hence (M @ ) *' = (M *' ) @ by A4, A5, A6, A7, MATRIX_1:21; :: thesis: verum