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;

.= len F by GROUP_4:def 3 ;

hence (F |^ a) |^ I = (F |^ I) |^ a by A2, A4, A6, FINSEQ_2:9; :: thesis: verum

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

len ((F |^ I) |^ a) =
len (F |^ I)
by Def1
((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;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

.= len F by GROUP_4:def 3 ;

hence (F |^ a) |^ I = (F |^ I) |^ a by A2, A4, A6, FINSEQ_2:9; :: thesis: verum