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 ;
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 ;
then A8: (F |^ a) /. k = (F |^ a) . k by ;
A9: (F |^ I) /. k = (F |^ I) . k by ;
thus ((F |^ a) |^ I) . k = ((F |^ a) /. k) |^ (@ (I /. k)) by
.= ((F /. k) |^ a) |^ (@ (I /. k)) by A7, A8, Def1
.= ((F /. k) |^ (@ (I /. k))) |^ a by GROUP_3:28
.= ((F |^ I) /. k) |^ a by
.= ((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 ; :: thesis: verum