theorem :: MATRIX_7:9

for n being Nat
for a, b being Element of (Group_of_Perm n)
for pa, pb being Element of Permutations n st a = pa & b = pb holds
a * b = pb * pa by MATRIX_1:def 13;