let a be Element of (Group_of_Perm 3); :: thesis: ( a = <*2,3,1*> implies a " = <*3,1,2*> )
reconsider a1 = a as Element of Permutations 3 by MATRIX_1:def 13;
assume a = <*2,3,1*> ; :: thesis: a " = <*3,1,2*>
then a1 " = <*3,1,2*> by Th28;
hence a " = <*3,1,2*> by MATRIX_7:27; :: thesis: verum