let G be Group; :: thesis: 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
let a be Element of G; :: thesis: for F being FinSequence of the carrier of G
for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a
let F be FinSequence of the carrier of G; :: thesis: for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a
let I be FinSequence of INT ; :: thesis: (F |^ a) |^ I = (F |^ I) |^ a
len (F |^ I) = len F by GROUP_4:def 3;
then A1: dom (F |^ I) = dom F by FINSEQ_3:29;
A2: len (F |^ a) = len F by Def1;
then A3: dom (F |^ a) = dom F by FINSEQ_3:29;
A4: len ((F |^ a) |^ I) = len (F |^ a) by GROUP_4:def 3;
then A5: dom ((F |^ a) |^ I) = Seg (len F) by A2, FINSEQ_1:def 3;

A6: now :: thesis: for k being Nat st k in dom ((F |^ a) |^ I) holds
((F |^ a) |^ I) . k = ((F |^ I) |^ a) . k

let k be Nat; :: thesis: ( k in dom ((F |^ a) |^ I) implies ((F |^ a) |^ I) . k = ((F |^ I) |^ a) . k )
assume k in dom ((F |^ a) |^ I) ; :: thesis: ((F |^ a) |^ I) . k = ((F |^ I) |^ a) . k
then A7: k in dom F by A5, FINSEQ_1:def 3;
then A8: (F |^ a) /. k = (F |^ a) . k by A3, PARTFUN1:def 6;
A9: (F |^ I) /. k = (F |^ I) . k by A1, A7, PARTFUN1:def 6;
thus ((F |^ a) |^ I) . k = ((F |^ a) /. k) |^ (@ (I /. k)) by A3, A7, GROUP_4:def 3
.= ((F /. k) |^ a) |^ (@ (I /. k)) by A7, A8, Def1
.= ((F /. k) |^ (@ (I /. k))) |^ a by GROUP_3:28
.= ((F |^ I) /. k) |^ a by A7, A9, GROUP_4:def 3
.= ((F |^ I) |^ a) . k by A1, A7, Def1 ; :: thesis: verum

end;

len ((F |^ I) |^ a) = len (F |^ I) by Def1
.= len F by GROUP_4:def 3 ;
hence (F |^ a) |^ I = (F |^ I) |^ a by A2, A4, A6, FINSEQ_2:9; :: thesis: verum