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

end;

len ((M *' ) @ ) = width (M *' ) by MATRIX_1:def 7
.= width M by Def1 ;
hence (M @ ) *' = (M *' ) @ by A4, A5, A2, A7, MATRIX_1:21; :: thesis: verum