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_0:54
.= len M by Def1 ;
A3: width ((M @) *') = width (M @) by Def1;
A4: len ((M @) *') = len (M @) by Def1
.= width M by MATRIX_0:def 6 ;
A5: width ((M @) *') = width (M @) by Def1
.= len M by A1, MATRIX_0:54 ;
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_0:def 6;
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_0:def 6
.= (M *') * (j,i) by A13, Def1
.= ((M *') @) * (i,j) by A17, MATRIX_0:def 6 ;
hence ((M @) *') * (i,j) = ((M *') @) * (i,j) ; :: thesis: verum

end;

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