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