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
A1: len (F |^ a) = len F by Def1;
then A2: dom (F |^ a) = dom F by FINSEQ_3:31;
A3: len ((F |^ a) |^ I) = len (F |^ a) by GROUP_4:def 4;
A4: len ((F |^ I) |^ a) = len (F |^ I) by Def1
.= len F by GROUP_4:def 4 ;
len (F |^ I) = len F by GROUP_4:def 4;
then A5: dom (F |^ I) = dom F by FINSEQ_3:31;
X: dom ((F |^ a) |^ I) = Seg (len F) by A3, A1, FINSEQ_1:def 3;

now

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 A6: k in dom F by X, FINSEQ_1:def 3;
then A7: ( (F |^ a) /. k = (F |^ a) . k & (F |^ I) /. k = (F |^ I) . k ) by A2, A5, PARTFUN1:def 8;
thus ((F |^ a) |^ I) . k = ((F |^ a) /. k) |^ (@ (I /. k)) by A2, A6, GROUP_4:def 4
.= ((F /. k) |^ a) |^ (@ (I /. k)) by A6, A7, Def1
.= ((F /. k) |^ (@ (I /. k))) |^ a by GROUP_3:34
.= ((F |^ I) /. k) |^ a by A6, A7, GROUP_4:def 4
.= ((F |^ I) |^ a) . k by A5, A6, Def1 ; :: thesis: verum

end;

hence (F |^ a) |^ I = (F |^ I) |^ a by A1, A3, A4, FINSEQ_2:10; :: thesis: verum