let G be 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
let a be 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 F be FinSequence of the carrier of G; for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a
let I be FinSequence of INT ; (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 for k being Nat st k in dom ((F |^ a) |^ I) holds
((F |^ a) |^ I) . k = ((F |^ I) |^ a) . klet k be
Nat;
( k in dom ((F |^ a) |^ I) implies ((F |^ a) |^ I) . k = ((F |^ I) |^ a) . k )assume
k in dom ((F |^ a) |^ I)
;
((F |^ a) |^ I) . k = ((F |^ I) |^ a) . kthen 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
;
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; verum