for G being Group
for a being Element of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a