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

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